Theorem pm2.61dan

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

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