Theorem bi2anan9r

Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 19-Feb-1996.)

Hypotheses
bi2an9.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
bi2an9.2
\( \vdash \theta \rightarrow (\tau \leftrightarrow \eta) \)
Conclusion
\( \vdash \theta \wedge \varphi \rightarrow (\psi \wedge \tau \leftrightarrow \chi \wedge \eta) \)
Proof
l0
bi2an9.1
bi2an9.2
bi2anan9 l0 _
ancoms _