Theorem mtbir

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

Hypotheses
mtbir.1
\( \vdash \neg \psi \)
mtbir.2
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \neg \varphi \)
Proof
l0
mtbir.1
\( \vdash \neg \psi \)
mtbir.2
bicomi _
\( \vdash \psi \leftrightarrow \varphi \)
mtbi l0 _