Theorem pm2.65i

Inference for proof by contradiction. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.) (Proof shortened by Garrett Katz, 7-Jun-2026.)

Hypotheses
pm2.65i.1
\( \vdash \varphi \rightarrow \psi \)
pm2.65i.2
\( \vdash \varphi \rightarrow \neg \psi \)
Conclusion
\( \vdash \neg \varphi \)
Proof
l0
pm2.65i.2
\( \vdash \varphi \rightarrow \neg \psi \)
pm2.65i.1
\( \vdash \varphi \rightarrow \psi \)
nsyl3 l0 _
pm2.01i _