Theorem mpbi2and

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

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