Theorem 3ancoma

Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 5-Jun-2022.)

Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \leftrightarrow \psi \wedge \varphi \wedge \chi \)
Proof
l0
3anan12
\( \vdash \varphi \wedge \psi \wedge \chi \leftrightarrow \psi \wedge (\varphi \wedge \chi) \)
3anass
\( \vdash \psi \wedge \varphi \wedge \chi \leftrightarrow \psi \wedge (\varphi \wedge \chi) \)
bitr4i l0 _