Theorem pm2.65iOLD

Obsolete version of pm2.65i as of 7-Jun-2026. Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses
pm2.65i.1
\( \vdash \varphi \rightarrow \psi \)
pm2.65i.2
\( \vdash \varphi \rightarrow \neg \psi \)
Conclusion
\( \vdash \neg \varphi \)
Proof
pm2.65i.2
l1
con2i _
\( \vdash \psi \rightarrow \neg \varphi \)
pm2.65i.1
con3i _
\( \vdash \neg \psi \rightarrow \neg \varphi \)
pm2.61i l1 _