Theorem con2i

A contraposition inference. Its associated inference is mt2. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Mel L. O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.)

Hypothesis
con2i.a
\( \vdash \varphi \rightarrow \neg \psi \)
Conclusion
\( \vdash \psi \rightarrow \neg \varphi \)
Proof
l0
con2i.a
\( \vdash \varphi \rightarrow \neg \psi \)
id
\( \vdash \psi \rightarrow \psi \)
nsyl3 l0 _