Theorem 3anbi2d

Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

Hypothesis
3anbi1d.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \rightarrow (\theta \wedge \psi \wedge \tau \leftrightarrow \theta \wedge \chi \wedge \tau) \)
Proof
l0
biidd
3anbi1d.1
3anbi12d l0 _