Theorem mpbir

An inference from a biconditional, related to modus ponens. (Contributed by NM, 28-Dec-1992.)

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