Theorem mtbi

An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses
mtbi.1
\( \vdash \neg \varphi \)
mtbi.2
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \neg \psi \)
Proof
l0
mtbi.1
\( \vdash \neg \varphi \)
mtbi.2
biimpri _
\( \vdash \psi \rightarrow \varphi \)
mto l0 _