Theorem 3anass

Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)

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