Theorem 3an4anass

Associative law for four conjunctions with a triple conjunction. (Contributed by Alexander van der Vekens, 24-Jun-2018.)

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