Theorem mpbir3and

Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.) (Revised by Mario Carneiro, 9-Jan-2015.)

Hypotheses
mpbir3and.1
\( \vdash \varphi \rightarrow \chi \)
mpbir3and.2
\( \vdash \varphi \rightarrow \theta \)
mpbir3and.3
\( \vdash \varphi \rightarrow \tau \)
mpbir3and.4
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \wedge \theta \wedge \tau) \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
mpbir3and.1
l1
mpbir3and.2
mpbir3and.3
l3
3jca l0 l1 _
\( \vdash \varphi \rightarrow \chi \wedge \theta \wedge \tau \)
mpbir3and.4
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \wedge \theta \wedge \tau) \)
mpbird l3 _