Theorem 3anbi12d

Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)

Hypotheses
3anbi12d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
3anbi12d.2
\( \vdash \varphi \rightarrow (\theta \leftrightarrow \tau) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \wedge \theta \wedge \eta \leftrightarrow \chi \wedge \tau \wedge \eta) \)
Proof
l0
3anbi12d.1
l1
3anbi12d.2
biidd
3anbi123d l0 l1 _