Theorem bi2anan9

Deduction joining two equivalences to form equivalence of conjunctions. (Contributed by NM, 31-Jul-1995.)

Hypotheses
bi2an9.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
bi2an9.2
\( \vdash \theta \rightarrow (\tau \leftrightarrow \eta) \)
Conclusion
\( \vdash \varphi \wedge \theta \rightarrow (\psi \wedge \tau \leftrightarrow \chi \wedge \eta) \)
Proof
l0
bi2an9.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
l1
bi2an9.2
\( \vdash \theta \rightarrow (\tau \leftrightarrow \eta) \)
pm4.38
\( \vdash (\psi \leftrightarrow \chi) \wedge (\tau \leftrightarrow \eta) \rightarrow (\psi \wedge \tau \leftrightarrow \chi \wedge \eta) \)
syl2an l0 l1 _