Theorem mtbii

An inference from a biconditional, similar to modus tollens. (Contributed by NM, 27-Nov-1995.)

Hypotheses
mtbii.min
\( \vdash \neg \psi \)
mtbii.maj
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow \neg \chi \)
Proof
l0
mtbii.min
\( \vdash \neg \psi \)
mtbii.maj
biimprd _
\( \vdash \varphi \rightarrow \chi \rightarrow \psi \)
mtoi l0 _