Theorem mpbidi

A deduction from a biconditional, related to modus ponens. (Contributed by NM, 9-Aug-1994.)

Hypotheses
mpbidi.min
\( \vdash \theta \rightarrow \varphi \rightarrow \psi \)
mpbidi.maj
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \theta \rightarrow \varphi \rightarrow \chi \)
Proof
l0
mpbidi.min
\( \vdash \theta \rightarrow \varphi \rightarrow \psi \)
mpbidi.maj
biimpd _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
sylcom l0 _