Theorem mpbir2and

Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypotheses
mpbir2and.1
\( \vdash \varphi \rightarrow \chi \)
mpbir2and.2
\( \vdash \varphi \rightarrow \theta \)
mpbir2and.3
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \wedge \theta) \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
mpbir2and.1
mpbir2and.2
l2
jca l0 _
\( \vdash \varphi \rightarrow \chi \wedge \theta \)
mpbir2and.3
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \wedge \theta) \)
mpbird l2 _