Theorem anandir

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

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