Theorem anandi3

Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018.)

Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \leftrightarrow \varphi \wedge \psi \wedge (\varphi \wedge \chi) \)
Proof
l0
3anass
\( \vdash \varphi \wedge \psi \wedge \chi \leftrightarrow \varphi \wedge (\psi \wedge \chi) \)
anandi
\( \vdash \varphi \wedge (\psi \wedge \chi) \leftrightarrow \varphi \wedge \psi \wedge (\varphi \wedge \chi) \)
bitri l0 _