Theorem 3ancomb

Commutation law for triple conjunction. (Contributed by NM, 21-Apr-1994.) (Revised to shorten 3anrot by Wolf Lammen, 9-Jun-2022.)

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