Theorem mtbiri

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

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