Theorem pm2.01d

Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.)

Hypothesis
pm2.01d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \psi \)
Conclusion
\( \vdash \varphi \rightarrow \neg \psi \)
Proof
l0
pm2.01d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \psi \)
id
\( \vdash \neg \psi \rightarrow \neg \psi \)
pm2.61d1 l0 _