Theorem con4i

Inference associated with con4. Its associated inference is mt4.

Remark: this can also be proved using notnot followed by nsyl2, giving a shorter proof but depending on more axioms (namely, [ax-1] and [ax-2] ). (Contributed by NM, 29-Dec-1992.)

Hypothesis
con4i.1
\( \vdash \neg \varphi \rightarrow \neg \psi \)
Conclusion
\( \vdash \psi \rightarrow \varphi \)
Proof
l0
con4i.1
\( \vdash \neg \varphi \rightarrow \neg \psi \)
con4
\( \vdash (\neg \varphi \rightarrow \neg \psi) \rightarrow \psi \rightarrow \varphi \)
ax-mp l0 _