Theorem 3anbi13d

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 \eta \wedge \theta \leftrightarrow \chi \wedge \eta \wedge \tau) \)
Proof
l0
3anbi12d.1
l1
biidd
3anbi12d.2
3anbi123d l0 l1 _