Theorem pm2.61ian

Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.)

Hypotheses
pm2.61ian.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
pm2.61ian.2
\( \vdash \neg \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \psi \rightarrow \chi \)
Proof
pm2.61ian.1
l1
ex _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
pm2.61ian.2
ex _
\( \vdash \neg \varphi \rightarrow \psi \rightarrow \chi \)
pm2.61i l1 _