Theorem an3andi

Distribution of conjunction over threefold conjunction. (Contributed by Thierry Arnoux, 8-Apr-2019.)

Conclusion
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \leftrightarrow \varphi \wedge \psi \wedge \varphi \wedge \chi \wedge \varphi \wedge \theta \)
Proof
l0
anandi
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \leftrightarrow \varphi \wedge (\psi \wedge \chi) \wedge (\varphi \wedge \theta) \)
anandi
\( \vdash \varphi \wedge (\psi \wedge \chi) \leftrightarrow \varphi \wedge \psi \wedge (\varphi \wedge \chi) \)
l2
bianbi l0 _
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \leftrightarrow \varphi \wedge \psi \wedge (\varphi \wedge \chi) \wedge (\varphi \wedge \theta) \)
df-3an
l4
anbi2i _
\( \vdash \varphi \wedge (\psi \wedge \chi \wedge \theta) \leftrightarrow \varphi \wedge (\psi \wedge \chi \wedge \theta) \)
df-3an
\( \vdash \varphi \wedge \psi \wedge \varphi \wedge \chi \wedge \varphi \wedge \theta \leftrightarrow \varphi \wedge \psi \wedge (\varphi \wedge \chi) \wedge (\varphi \wedge \theta) \)
3bitr4i l2 l4 _