Theorem an4

Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994.)

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