Theorem con3

Contraposition. Theorem *2.16 of [WhiteheadRussell] p. 103. This was the fourth axiom of Frege, specifically Proposition 28 of [Frege1879] p. 43. Its associated inference is con3i. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 13-Feb-2013.)

Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \varphi \)
Proof
id
con3d _