I've been playing around with another proof and I'm wondering if it's an OK way to approach the proof? Is there some reason that it causes problems? All suggestions and thoughts are welcome.
Proof sketch: We want to show that the following inference rule, SR, is sound:
$\begin{array}{lrlll} .&&&.\\ .&&&.\\ i.&\Gamma\cup\{\phi\}&\vdash&\psi\\ .&&&.\\ .&&&.\\ n.&\Gamma\cup\{\lnot\phi\}&\vdash&\psi&\\ n+1.&\Gamma&\vdash&\psi&\tiny\text{i, n, SR}\\ \end{array}$
Let $\phi$ and $\psi$ be wffs in classic propositional logic, and let $\Gamma$ be a set of wffs. Assume that the derivations on lines $i$ and $n$ are valid and $\psi$ is true.
If $\phi$ is true, then $\lnot\phi$ is false and $\psi$ is true. If $\phi$ is false, then $\lnot\phi$ is true and $\psi$ is true. Thus, $\psi$ is true regardless of the valuation of $\phi$ or $\lnot\phi$. As lines $i$ and $n$ are valid, $\psi$ must be dependent on some subset of $\Gamma$. As $\psi$ is dependent on $\Gamma$ and not $\phi$ or $\lnot\phi$, line $n+1$ is valid.
Idea behind it: I was reading about supervalution in trivalent logic and I wondered if I could use a similar idea to prove a wff and it's negation were independent and could be discharged. It also seemed reasonable that if weakening is allowed that there should be a way to reverse it. Another reason behind this is I wanted to prove $\phi\lor\lnot\phi$ without using double negation, which this inference rule would achieve. It also simplifies and improves the readability of other proofs.
P.S., It's pretty easy to show as a derived rule as it's just theorem introduction followed by disjunction elimination. Or we can go down the reductio route and it has the same pattern as proving $\phi\lor\lnot\phi$ - which is to say, it's definitely valid as a derived rule.