Theorem anandi

Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)

Conclusion
\( \vdash \varphi \wedge (\psi \wedge \chi) \leftrightarrow \varphi \wedge \psi \wedge (\varphi \wedge \chi) \)
Proof
anidm
l1
anbi1i _
\( \vdash \varphi \wedge \varphi \wedge (\psi \wedge \chi) \leftrightarrow \varphi \wedge (\psi \wedge \chi) \)
an4
\( \vdash \varphi \wedge \varphi \wedge (\psi \wedge \chi) \leftrightarrow \varphi \wedge \psi \wedge (\varphi \wedge \chi) \)
bitr3i l1 _