Theorem mpbir3an

Detach a conjunction of truths in a biconditional. (Contributed by NM, 16-Sep-2011.)

Hypotheses
mpbir3an.1
\( \vdash \psi \)
mpbir3an.2
\( \vdash \chi \)
mpbir3an.3
\( \vdash \theta \)
mpbir3an.4
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \wedge \theta \)
Conclusion
\( \vdash \varphi \)
Proof
l0
mpbir3an.1
l1
mpbir3an.2
mpbir3an.3
l3
3pm3.2i l0 l1 _
\( \vdash \psi \wedge \chi \wedge \theta \)
mpbir3an.4
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \wedge \theta \)
mpbir l3 _