Theorem con3i

A contraposition inference. Inference associated with con3. Its associated inference is mto. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)

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