Theorem anbi1

Introduce a right conjunct to both sides of a logical equivalence. Theorem *4.36 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)

Conclusion
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow (\varphi \wedge \chi \leftrightarrow \psi \wedge \chi) \)
Proof
id
anbi1d _