Theorem pm2.18da

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

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