I was given the following problem:
Find a derivation for$\{\varphi \Rightarrow (\psi \land \phi)\} \vdash \psi \Rightarrow (\varphi \Rightarrow \phi)$
The derivation is to be made using natural deduction. I came to the following derivation:
However, I am unsure of the last step ($\Rightarrow I$). It is the case that $\psi$ was found to be true; namely, when we arrived to $\psi \land \phi$. So the conclusion seems correct from an intuitive point of view. But I think the formal application of the rule is incorrect. The rule for $\Rightarrow I$ states that
If $[\varphi] \ldots \phi $ is a derivation, then $\varphi \Rightarrow \phi$.
In our case, I should have gotten a derivation of the form $\psi \ldots (\varphi \Rightarrow \phi)$, but what I have is a derivation of the form $(\psi \land \phi) \ldots (\varphi \Rightarrow \phi)$, which is not identical to what is stated in the rule.
Of course, another rule is $\land E$, by virtue of which $\psi$ follows from $\psi \land \phi$, but I have never applied this rule explicitly for $\psi$ (only for $\phi$).
It does not matter whether you have derived the antecedent or not. When the consequent is derived, then the conditional can be derived too. (Anything will imply a truth.)
Thus, this is usually considered a valid application of the rule of conditional introduction.
$$\def\implies{\mathop{\Rightarrow}} \dfrac{\vdots\\q}{~p\implies q~}{\small(\implies\mathsf I)}$$
You may discharge any number assumptions of the antecedent occurring above the line, including none.
However some proof checkers do have stricter requirements, and so only accept a discharge of one and only one assumption, Still, you may always add assumptions.
$$\dfrac{~\lower{2.5ex}{[p]^n}\quad{\vdots\\q}~}{p\implies q}{\small(\implies\mathsf I^n)}$$
Unless your source gives alternatives, your system appears to insist on a strict implementation of the rule. Your assignment marker may do so too. If so, then you should add the assumption and discharge it.