Theorem mpbiran

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

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