Sequents: if-introduction and discharging assumptions I am reading through "Mathematical Logic by Ian Chiswell & Wilfred Hodges"(amazon, and publisher)
for context I am reading through this for self-study, so I don't have the normal support of a classroom environment - and the lack of exercise solutions makes it hard to check my understanding.
 
On page 21 there is Exercise 2.4.4.f which asks "write out a derivation to prove the following sequent"
$\{(\phi \rightarrow (\psi \rightarrow \chi))\} \vdash ((\phi \wedge \psi) \rightarrow \chi)$
So far we have covered $\rightarrow$-Introduction and discharging in the following form
$$\begin{array}{lr}
\phi & \psi\\
\hline
 & (\phi \rightarrow \psi) \\
\end{array}
$$
which will discharge $\phi$ using $\rightarrow$-Introduction

My solution to 2.4.4.f so far is
(f) derivation of sequent $ \{ (\phi \rightarrow (\psi \rightarrow \chi)) \} \vdash ((\phi \wedge \psi) \rightarrow \chi) $
$$
\begin{array}{rrr}
\phi & & (\phi \rightarrow (\psi \rightarrow \chi)) \\
\hline
 \psi & & (\psi \rightarrow \chi) \\
\hline
 & & \chi
\end{array}
$$
which now leaves us with the undischarged assumptions
$ \{\phi, \psi, (\phi \rightarrow (\psi \rightarrow \chi)) \} $
from this I have $\chi$ so I can then (using $\rightarrow$-introduction)
$$
\begin{array}{r}
\chi \\
\hline
((\phi \wedge \psi) \rightarrow \chi) \\
\end{array}
$$
I don't have to discharge $(\phi \rightarrow (\psi \rightarrow \chi))$ as it is captured in the LHS of the sequent - but I do have to discharge both $\phi$ and $\psi$
In my $\rightarrow$-introduction above this means I can then discharge $(\phi \wedge \psi)$, but by the rules given so far it doesn't mean I can discharge $\phi$ and $\psi$ even though I know they are logically equivalent - that is if we can assume $(\phi \wedge \psi)$ then it is easy to show this entails both $\phi$ and $\psi$
Is it allowable to use $\rightarrow$-introduction of $(\phi \wedge \psi)$ to then discharge the assumptions of both $\phi$ and $\psi$ ?
If so, what is the generalisation of this ?
If not, how can I correctly form a derivation to prove this sequent?
 A: @MauroALLEGRANZA said:
'You have to start from $(\phi \wedge \psi)$ and then "unpack" it with $\wedge$-elim to get $\phi$ and $\psi$ separately. Then you can go on with the first part of your derivation.'
This answer tries to capture that technique

2.4.4.f is to prove $\{(\phi \rightarrow (\psi \rightarrow \chi))\} \vdash ((\phi \wedge \psi) \rightarrow \chi)$
$\wedge$-elim to get $\phi$ :
$$
\begin{array}{c}
(\phi \wedge \psi) \\
\hline
\phi
\end{array}
$$
$\wedge$-elim to get $\psi$ :
$$
\begin{array}{c}
(\phi \wedge \psi) \\
\hline
\psi
\end{array}
$$
and now the derivation
the above 2 derivations allow us to discharge $\phi$ and $\psi$
$$
\begin{array}{rrr}
\phi & & (\phi \rightarrow (\psi \rightarrow \chi)) \\
\hline
\psi & & (\psi \rightarrow \chi) \\
\hline
 & & \chi \\
\hline
 & & ((\phi \wedge \psi) \rightarrow \chi) \\
\end{array}
$$
which shows we can derive the sequent $((\phi \wedge \psi) \rightarrow \chi)$ with the undisharged assumptions of $\{ (\phi \rightarrow (\psi \rightarrow \chi))\}$
Thus proving the sequent
$\{(\phi \rightarrow (\psi \rightarrow \chi))\} \vdash ((\phi \wedge \psi) \rightarrow \chi)$
A: It is helpful to indicate what assumptions are being discharged and where; usually by indices and either canceling or boxing off the assumption.   So conditional introduction should be presented similar to: $$\require{cancel}\dfrac{\cancel{~\phi~}^n\quad\psi}{\phi\to\psi}{\small{\to}\mathsf I^n}\qquad\dfrac{[\phi]^n\quad\psi}{\phi\to\psi}{\small{\to}\mathsf I^n}\\~\\\tiny\text{NB: I prefer boxing, as it is cleaner.}$$
Why is this helpful? Well, the assumption may not appear immediately above the line in which it is discharged; and may appear multiple times.  
In this case, you seek to discharge $\phi\land\psi$ so to introduce the conditional; further, the only assumption that should remain undischarged at the end of the proof is the premise $\phi\to(\psi\to\chi)$.  So you cannot leave the $\phi$ and $\psi$ naked; they must be covered by the discharged assumption; ie: you must derive them using conjunction elimination.
$$\dfrac{\dfrac{\dfrac{\lower{1.5ex}{\phi\to(\psi\to\chi)}\quad\dfrac{[\phi\land\psi]^1}{\phi}{\small\land\mathsf E}}{\psi\to\chi}{\small{\to}\mathsf E}\quad\dfrac{[\phi\land\psi]^1}{\psi}{\small\land\mathsf E}~}{\chi}{\small{\to}\mathsf E}}{(\phi\land\psi)\to\chi}{\small{\to}\mathsf I^1}$$

In Fitch style, this proof would look like$$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{~~1.~~\phi\to(\psi\to\chi)}{\fitch{~~2.~~\phi\land\psi}{~~3.~~\psi\hspace{12ex}{\land}\mathsf E~2\\~~4.~~\phi\hspace{12ex}{\land}\mathsf E~2\\~~5.~~\psi\to\chi\hspace{7ex}{\to}\mathsf E~4,1\\~~6.~~\chi\hspace{12ex}{\to}\mathsf E~3,5}\\~~7.~~(\phi\land\psi)\to\chi\hspace{4ex}{\to}\mathsf I~2{-}6}$$
So the assumption is raised in line 2, used twice (in lines 3 and 4), and discharged for line 7
