Theorem con1i

A contraposition inference. Inference associated with con1. Its associated inference is mt3. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 19-Jun-2013.)

Hypothesis
con1i.1
\( \vdash \neg \varphi \rightarrow \psi \)
Conclusion
\( \vdash \neg \psi \rightarrow \varphi \)
Proof
l0
id
\( \vdash \neg \psi \rightarrow \neg \psi \)
con1i.1
\( \vdash \neg \varphi \rightarrow \psi \)
nsyl2 l0 _