Theorem mtbid

A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 26-Nov-1995.)

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