Theorem mt3

A rule similar to modus tollens. Inference associated with con1i. (Contributed by NM, 18-May-1994.) (Proof shortened by Wolf Lammen, 11-Sep-2013.)

Hypotheses
mt3.1
\( \vdash \neg \psi \)
mt3.2
\( \vdash \neg \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \)
Proof
l0
mt3.1
\( \vdash \neg \psi \)
mt3.2
\( \vdash \neg \varphi \rightarrow \psi \)
mto l0 _
notnotri _