Theorem an33rean
Rearrange a 9-fold conjunction. (Contributed by Thierry Arnoux,
14-Apr-2019.) (Proof shortened by Wolf Lammen, 21-Apr-2024.)
Conclusion
\( \vdash (\varphi \wedge \psi \wedge \chi) \wedge (\theta \wedge \tau \wedge \eta) \wedge (\zeta \wedge \sigma \wedge \rho) \leftrightarrow (\varphi \wedge \tau \wedge \rho) \wedge (\psi \wedge \theta \wedge \eta \wedge \sigma \wedge \chi \wedge \zeta) \)
Proof
l0
3anass
l1
3anan12
l2
3anrev
\( \vdash \zeta \wedge \sigma \wedge \rho \leftrightarrow \rho \wedge \sigma \wedge \zeta \)
3anass
\( \vdash \rho \wedge \sigma \wedge \zeta \leftrightarrow \rho \wedge (\sigma \wedge \zeta) \)
bitri l2 _
l5
3anbi123i l0 l1 _
\( \vdash (\varphi \wedge \psi \wedge \chi) \wedge (\theta \wedge \tau \wedge \eta) \wedge (\zeta \wedge \sigma \wedge \rho) \leftrightarrow \varphi \wedge (\psi \wedge \chi) \wedge \tau \wedge (\theta \wedge \eta) \wedge \rho \wedge (\sigma \wedge \zeta) \)
l6
3an6
\( \vdash \varphi \wedge (\psi \wedge \chi) \wedge \tau \wedge (\theta \wedge \eta) \wedge \rho \wedge (\sigma \wedge \zeta) \leftrightarrow (\varphi \wedge \tau \wedge \rho) \wedge (\psi \wedge \chi \wedge \theta \wedge \eta \wedge \sigma \wedge \zeta) \)
anass
l8
anbi2i _
\( \vdash \psi \wedge \chi \wedge (\theta \wedge \eta \wedge \sigma) \leftrightarrow \psi \wedge \chi \wedge (\theta \wedge (\eta \wedge \sigma)) \)
an42
\( \vdash \psi \wedge \chi \wedge (\theta \wedge (\eta \wedge \sigma)) \leftrightarrow \psi \wedge \theta \wedge (\eta \wedge \sigma \wedge \chi) \)
l10
bitri l8 _
\( \vdash \psi \wedge \chi \wedge (\theta \wedge \eta \wedge \sigma) \leftrightarrow \psi \wedge \theta \wedge (\eta \wedge \sigma \wedge \chi) \)
l11
anass
\( \vdash \psi \wedge \chi \wedge (\theta \wedge \eta) \wedge \sigma \leftrightarrow \psi \wedge \chi \wedge (\theta \wedge \eta \wedge \sigma) \)
anass
\( \vdash \psi \wedge \theta \wedge (\eta \wedge \sigma) \wedge \chi \leftrightarrow \psi \wedge \theta \wedge (\eta \wedge \sigma \wedge \chi) \)
3bitr4i l10 l11 _
l14
anbi1i _
\( \vdash \psi \wedge \chi \wedge (\theta \wedge \eta) \wedge \sigma \wedge \zeta \leftrightarrow \psi \wedge \theta \wedge (\eta \wedge \sigma) \wedge \chi \wedge \zeta \)
l15
anass
\( \vdash \psi \wedge \chi \wedge (\theta \wedge \eta) \wedge \sigma \wedge \zeta \leftrightarrow \psi \wedge \chi \wedge (\theta \wedge \eta) \wedge (\sigma \wedge \zeta) \)
anass
\( \vdash \psi \wedge \theta \wedge (\eta \wedge \sigma) \wedge \chi \wedge \zeta \leftrightarrow \psi \wedge \theta \wedge (\eta \wedge \sigma) \wedge (\chi \wedge \zeta) \)
l17
3bitr3i l14 l15 _
\( \vdash \psi \wedge \chi \wedge (\theta \wedge \eta) \wedge (\sigma \wedge \zeta) \leftrightarrow \psi \wedge \theta \wedge (\eta \wedge \sigma) \wedge (\chi \wedge \zeta) \)
l18
df-3an
\( \vdash \psi \wedge \chi \wedge \theta \wedge \eta \wedge \sigma \wedge \zeta \leftrightarrow \psi \wedge \chi \wedge (\theta \wedge \eta) \wedge (\sigma \wedge \zeta) \)
df-3an
\( \vdash \psi \wedge \theta \wedge \eta \wedge \sigma \wedge \chi \wedge \zeta \leftrightarrow \psi \wedge \theta \wedge (\eta \wedge \sigma) \wedge (\chi \wedge \zeta) \)
3bitr4i l17 l18 _
anbi2i _
\( \vdash (\varphi \wedge \tau \wedge \rho) \wedge (\psi \wedge \chi \wedge \theta \wedge \eta \wedge \sigma \wedge \zeta) \leftrightarrow (\varphi \wedge \tau \wedge \rho) \wedge (\psi \wedge \theta \wedge \eta \wedge \sigma \wedge \chi \wedge \zeta) \)
3bitri l5 l6 _