Theorem mtbird

A deduction from a biconditional, similar to modus tollens. (Contributed by NM, 10-May-1994.)

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