Theorem 3anan12

Convert triple conjunction to conjunction, then commute. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) (Revised to shorten 3ancoma by Wolf Lammen, 5-Jun-2022.)

Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \leftrightarrow \psi \wedge (\varphi \wedge \chi) \)
Proof
l0
3anass
\( \vdash \varphi \wedge \psi \wedge \chi \leftrightarrow \varphi \wedge (\psi \wedge \chi) \)
an12
\( \vdash \varphi \wedge (\psi \wedge \chi) \leftrightarrow \psi \wedge (\varphi \wedge \chi) \)
bitri l0 _