Theorem ancom

Commutative law for conjunction. Theorem *4.3 of [WhiteheadRussell] p. 118. (Contributed by NM, 25-Jun-1998.) (Proof shortened by Wolf Lammen, 4-Nov-2012.)

Conclusion
\( \vdash \varphi \wedge \psi \leftrightarrow \psi \wedge \varphi \)
Proof
l0
pm3.22
pm3.22
impbii l0 _