Theorem 3anbi1d

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 (\psi \wedge \theta \wedge \tau \leftrightarrow \chi \wedge \theta \wedge \tau) \)
Proof
l0
3anbi1d.1
biidd
3anbi12d l0 _