Theorem an42

Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996.)

Conclusion
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \leftrightarrow \varphi \wedge \chi \wedge (\theta \wedge \psi) \)
Proof
l0
an4
\( \vdash \varphi \wedge \psi \wedge (\chi \wedge \theta) \leftrightarrow \varphi \wedge \chi \wedge (\psi \wedge \theta) \)
ancom
anbi2i _
\( \vdash \varphi \wedge \chi \wedge (\psi \wedge \theta) \leftrightarrow \varphi \wedge \chi \wedge (\theta \wedge \psi) \)
bitri l0 _