Theorem 3anan32OLD

Obsolete version of 3anan32 as of 15-Jun-2026. Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.) (Proof modification is discouraged.)

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 \)
an32
\( \vdash \varphi \wedge \psi \wedge \chi \leftrightarrow \varphi \wedge \chi \wedge \psi \)
bitri l0 _