Theorem bi2bian9

Deduction joining two biconditionals with different antecedents. (Contributed by NM, 12-May-2004.)

Hypotheses
bi2an9.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
bi2an9.2
\( \vdash \theta \rightarrow (\tau \leftrightarrow \eta) \)
Conclusion
\( \vdash \varphi \wedge \theta \rightarrow (\psi \leftrightarrow \tau \leftrightarrow (\chi \leftrightarrow \eta)) \)
Proof
bi2an9.1
l1
adantr _
bi2an9.2
adantl _
bibi12d l1 _