discharge assumption in another branch I am self studying from Chiswell & Hodges mathematical logic, and I have a general question about discharging assumptions. To demonstrate, I am using exercise 2.5.1(c), which asks for a proof of:
$$\{(\phi \leftrightarrow \psi),(\psi \leftrightarrow \chi)\} \vdash ((\phi \leftrightarrow \chi)$$
I apologize for posting a possible solution via imgur, but I couldn't figure out how to label the rules beside the horizontal lines in Tex.
solution for exercise
QUESTION: can I discharge an assumption in a different branch of the overall derivation than where the discharge occurs? (see picture) i.e. can I discharge the $\phi$ in the right branch with the $(\rightarrow I)$ in the left branch?
P.S. I know the provided solution is wrong; in the right branch I struggled to obtain $\phi$ for $(\chi\rightarrow\phi)$, but eventually solved it in a self-contained manner. However, it did raise the question above, and I wanted to confirm that such an option was not possible.
P.P.S. I am aware of this question, but I feel that it does not quite answer mine, and wanted further clarity.
 A: I recommend you learn Fitch-style natural deduction as well (see examples and rules), which show explicitly the context of every single statement. This would also make clear precisely what is going on in tree-style natural deduction. Specifically, discharging an assumption corresponds to coming out from under the context of that assumption.
Here is the Fitch-style proof:
$
\def\eq{\leftrightarrow}
$

$P \eq Q$.
$Q \eq R$.
$P \to Q$.
$Q \to R$.
If $P$:
  $Q$.
  $R$.
$P \to R$.   [(1)]
[... Similarly ...]
$R \to P$.
$P \eq R$.

As you can see, the $\to$-introduction at (1) corresponds exactly to what is called 'discharging of $P$' in tree-style natural deduction. Importantly, you can also see that according to the rules you cannot 'discharge $P$' at other places. It makes no sense anyway.
An in-between alternative is sequent-style natural deduction as described in Rautenberg's Concise Introduction to Mathematical Logic. Either form of natural deduction will also make it easy to understand Hilbert-style systems for first-order logic, which are otherwise rather opaque.
