Theorem mpbid

A deduction from a biconditional, related to modus ponens. (Contributed by NM, 21-Jun-1993.)

Hypotheses
mpbid.min
\( \vdash \varphi \rightarrow \psi \)
mpbid.maj
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
mpbid.min
\( \vdash \varphi \rightarrow \psi \)
mpbid.maj
biimpd _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
mpd l0 _