Theorem con1

Contraposition. Theorem *2.15 of [WhiteheadRussell] p. 102. Its associated inference is con1i. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 12-Feb-2013.)

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