Theorem mpbird

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

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