Theorem an31

A rearrangement of conjuncts. (Contributed by NM, 24-Jun-2012.) (Proof shortened by Wolf Lammen, 31-Dec-2012.)

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