Theorem mt4

The rule of modus tollens. Inference associated with con4i. (Contributed by Wolf Lammen, 12-May-2013.)

Hypotheses
mt4.1
\( \vdash \varphi \)
mt4.2
\( \vdash \neg \psi \rightarrow \neg \varphi \)
Conclusion
\( \vdash \psi \)
Proof
l0
mt4.1
\( \vdash \varphi \)
mt4.2
con4i _
\( \vdash \varphi \rightarrow \psi \)
ax-mp l0 _