Theorem anbi12d

Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 26-May-1993.)

Hypotheses
anbi12d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
anbi12d.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \wedge \theta \leftrightarrow \chi \wedge \tau) \)
Proof
anbi12d.1
l1
anbi1d _
\( \vdash \varphi \rightarrow (\psi \wedge \theta \leftrightarrow \chi \wedge \theta) \)
anbi12d.2
anbi2d _
\( \vdash \varphi \rightarrow (\chi \wedge \theta \leftrightarrow \chi \wedge \tau) \)
bitrd l1 _