Theorem pm2.65da

Deduction for proof by contradiction. (Contributed by NM, 12-Jun-2014.)

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