Theorem mpbi

An inference from a biconditional, related to modus ponens. (Contributed by NM, 11-May-1993.)

Hypotheses
mpbi.min
\( \vdash \varphi \)
mpbi.maj
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \psi \)
Proof
l0
mpbi.min
\( \vdash \varphi \)
mpbi.maj
biimpi _
\( \vdash \varphi \rightarrow \psi \)
ax-mp l0 _