an33rean

Description: Rearrange a 9-fold conjunction. (Contributed by Thierry Arnoux, 14-Apr-2019) (Proof shortened by Wolf Lammen, 21-Apr-2024)

		Ref	Expression
	Assertion	an33rean	$⊢ ((φ \land ψ \land χ) \land (θ \land τ \land η) \land (ζ \land σ \land ρ)) \leftrightarrow ((φ \land τ \land ρ) \land ((ψ \land θ) \land (η \land σ) \land (χ \land ζ)))$

Proof

Step	Hyp	Ref	Expression
1		3anass	$⊢ (φ \land ψ \land χ) \leftrightarrow (φ \land (ψ \land χ))$
2		3anan12	$⊢ (θ \land τ \land η) \leftrightarrow (τ \land (θ \land η))$
3		3anrev	$⊢ (ζ \land σ \land ρ) \leftrightarrow (ρ \land σ \land ζ)$
4		3anass	$⊢ (ρ \land σ \land ζ) \leftrightarrow (ρ \land (σ \land ζ))$
5	3 4	bitri	$⊢ (ζ \land σ \land ρ) \leftrightarrow (ρ \land (σ \land ζ))$
6	1 2 5	3anbi123i	$⊢ ((φ \land ψ \land χ) \land (θ \land τ \land η) \land (ζ \land σ \land ρ)) \leftrightarrow ((φ \land (ψ \land χ)) \land (τ \land (θ \land η)) \land (ρ \land (σ \land ζ)))$
7		3an6	$⊢ ((φ \land (ψ \land χ)) \land (τ \land (θ \land η)) \land (ρ \land (σ \land ζ))) \leftrightarrow ((φ \land τ \land ρ) \land ((ψ \land χ) \land (θ \land η) \land (σ \land ζ)))$
8		anass	$⊢ ((θ \land η) \land σ) \leftrightarrow (θ \land (η \land σ))$
9	8	anbi2i	$⊢ ((ψ \land χ) \land ((θ \land η) \land σ)) \leftrightarrow ((ψ \land χ) \land (θ \land (η \land σ)))$
10		an42	$⊢ ((ψ \land χ) \land (θ \land (η \land σ))) \leftrightarrow ((ψ \land θ) \land ((η \land σ) \land χ))$
11	9 10	bitri	$⊢ ((ψ \land χ) \land ((θ \land η) \land σ)) \leftrightarrow ((ψ \land θ) \land ((η \land σ) \land χ))$
12		anass	$⊢ (((ψ \land χ) \land (θ \land η)) \land σ) \leftrightarrow ((ψ \land χ) \land ((θ \land η) \land σ))$
13		anass	$⊢ (((ψ \land θ) \land (η \land σ)) \land χ) \leftrightarrow ((ψ \land θ) \land ((η \land σ) \land χ))$
14	11 12 13	3bitr4i	$⊢ (((ψ \land χ) \land (θ \land η)) \land σ) \leftrightarrow (((ψ \land θ) \land (η \land σ)) \land χ)$
15	14	anbi1i	$⊢ ((((ψ \land χ) \land (θ \land η)) \land σ) \land ζ) \leftrightarrow ((((ψ \land θ) \land (η \land σ)) \land χ) \land ζ)$
16		anass	$⊢ ((((ψ \land χ) \land (θ \land η)) \land σ) \land ζ) \leftrightarrow (((ψ \land χ) \land (θ \land η)) \land (σ \land ζ))$
17		anass	$⊢ ((((ψ \land θ) \land (η \land σ)) \land χ) \land ζ) \leftrightarrow (((ψ \land θ) \land (η \land σ)) \land (χ \land ζ))$
18	15 16 17	3bitr3i	$⊢ (((ψ \land χ) \land (θ \land η)) \land (σ \land ζ)) \leftrightarrow (((ψ \land θ) \land (η \land σ)) \land (χ \land ζ))$
19		df-3an	$⊢ ((ψ \land χ) \land (θ \land η) \land (σ \land ζ)) \leftrightarrow (((ψ \land χ) \land (θ \land η)) \land (σ \land ζ))$
20		df-3an	$⊢ ((ψ \land θ) \land (η \land σ) \land (χ \land ζ)) \leftrightarrow (((ψ \land θ) \land (η \land σ)) \land (χ \land ζ))$
21	18 19 20	3bitr4i	$⊢ ((ψ \land χ) \land (θ \land η) \land (σ \land ζ)) \leftrightarrow ((ψ \land θ) \land (η \land σ) \land (χ \land ζ))$
22	21	anbi2i	$⊢ ((φ \land τ \land ρ) \land ((ψ \land χ) \land (θ \land η) \land (σ \land ζ))) \leftrightarrow ((φ \land τ \land ρ) \land ((ψ \land θ) \land (η \land σ) \land (χ \land ζ)))$
23	6 7 22	3bitri	$⊢ ((φ \land ψ \land χ) \land (θ \land τ \land η) \land (ζ \land σ \land ρ)) \leftrightarrow ((φ \land τ \land ρ) \land ((ψ \land θ) \land (η \land σ) \land (χ \land ζ)))$

Metamath Proof Explorer

Theorem an33rean

Proof