Theorem an13

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
an21
\( \vdash \psi \wedge \varphi \wedge \chi \leftrightarrow \varphi \wedge (\psi \wedge \chi) \)
ancom
\( \vdash \psi \wedge \varphi \wedge \chi \leftrightarrow \chi \wedge (\psi \wedge \varphi) \)
bitr3i l0 _