Theorem mpbiran2

Detach truth from conjunction in biconditional. (Contributed by NM, 22-Feb-1996.)

Hypotheses
mpbiran2.1
\( \vdash \chi \)
mpbiran2.2
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
Conclusion
\( \vdash \varphi \leftrightarrow \psi \)
Proof
l0
mpbiran2.1
\( \vdash \chi \)
mpbiran2.2
biancomi _
\( \vdash \varphi \leftrightarrow \chi \wedge \psi \)
mpbiran l0 _