Theorem an6

Rearrangement of 6 conjuncts. (Contributed by NM, 13-Mar-1995.)

Conclusion
\( \vdash (\varphi \wedge \psi \wedge \chi) \wedge (\theta \wedge \tau \wedge \eta) \leftrightarrow \varphi \wedge \theta \wedge \psi \wedge \tau \wedge \chi \wedge \eta \)
Proof
l0
an4
\( \vdash \varphi \wedge \psi \wedge \chi \wedge (\theta \wedge \tau \wedge \eta) \leftrightarrow \varphi \wedge \psi \wedge (\theta \wedge \tau) \wedge (\chi \wedge \eta) \)
an4
\( \vdash \varphi \wedge \psi \wedge (\theta \wedge \tau) \leftrightarrow \varphi \wedge \theta \wedge (\psi \wedge \tau) \)
l2
bianbi l0 _
\( \vdash \varphi \wedge \psi \wedge \chi \wedge (\theta \wedge \tau \wedge \eta) \leftrightarrow \varphi \wedge \theta \wedge (\psi \wedge \tau) \wedge (\chi \wedge \eta) \)
l3
df-3an
df-3an
l5
anbi12i l3 _
\( \vdash (\varphi \wedge \psi \wedge \chi) \wedge (\theta \wedge \tau \wedge \eta) \leftrightarrow \varphi \wedge \psi \wedge \chi \wedge (\theta \wedge \tau \wedge \eta) \)
df-3an
\( \vdash \varphi \wedge \theta \wedge \psi \wedge \tau \wedge \chi \wedge \eta \leftrightarrow \varphi \wedge \theta \wedge (\psi \wedge \tau) \wedge (\chi \wedge \eta) \)
3bitr4i l2 l5 _