Theorem pm2.01da

Deduction based on reductio ad absurdum. See pm2.01. (Contributed by Mario Carneiro, 9-Feb-2017.)

Hypothesis
pm2.01da.1
\( \vdash \varphi \wedge \psi \rightarrow \neg \psi \)
Conclusion
\( \vdash \varphi \rightarrow \neg \psi \)
Proof
pm2.01da.1
ex _
pm2.01d _