Theorem pm2.65

Theorem *2.65 of [WhiteheadRussell] p. 107. Proof by contradiction. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 8-Mar-2013.)

Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \neg \psi) \rightarrow \neg \varphi \)
Proof
l0
idd
con3
jad l0 _