an33reanOLD

Description: Obsolete version of an33rean as of 21-Apr-2024. (Contributed by Thierry Arnoux, 14-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	an33reanOLD	$⊢ ((φ \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		an4	$⊢ ((θ \land η) \land (σ \land ζ)) \leftrightarrow ((θ \land σ) \land (η \land ζ))$
9	8	anbi2i	$⊢ ((ψ \land χ) \land ((θ \land η) \land (σ \land ζ))) \leftrightarrow ((ψ \land χ) \land ((θ \land σ) \land (η \land ζ)))$
10		3anass	$⊢ ((ψ \land χ) \land (θ \land η) \land (σ \land ζ)) \leftrightarrow ((ψ \land χ) \land ((θ \land η) \land (σ \land ζ)))$
11		3anass	$⊢ ((ψ \land χ) \land (θ \land σ) \land (η \land ζ)) \leftrightarrow ((ψ \land χ) \land ((θ \land σ) \land (η \land ζ)))$
12	9 10 11	3bitr4i	$⊢ ((ψ \land χ) \land (θ \land η) \land (σ \land ζ)) \leftrightarrow ((ψ \land χ) \land (θ \land σ) \land (η \land ζ))$
13		an4	$⊢ ((ψ \land χ) \land (θ \land σ)) \leftrightarrow ((ψ \land θ) \land (χ \land σ))$
14	13	anbi1i	$⊢ (((ψ \land χ) \land (θ \land σ)) \land (η \land ζ)) \leftrightarrow (((ψ \land θ) \land (χ \land σ)) \land (η \land ζ))$
15		df-3an	$⊢ ((ψ \land χ) \land (θ \land σ) \land (η \land ζ)) \leftrightarrow (((ψ \land χ) \land (θ \land σ)) \land (η \land ζ))$
16		df-3an	$⊢ ((ψ \land θ) \land (χ \land σ) \land (η \land ζ)) \leftrightarrow (((ψ \land θ) \land (χ \land σ)) \land (η \land ζ))$
17	14 15 16	3bitr4i	$⊢ ((ψ \land χ) \land (θ \land σ) \land (η \land ζ)) \leftrightarrow ((ψ \land θ) \land (χ \land σ) \land (η \land ζ))$
18		3ancomb	$⊢ (ψ \land χ \land η) \leftrightarrow (ψ \land η \land χ)$
19	18	anbi1i	$⊢ ((ψ \land χ \land η) \land (θ \land σ \land ζ)) \leftrightarrow ((ψ \land η \land χ) \land (θ \land σ \land ζ))$
20		3an6	$⊢ ((ψ \land θ) \land (χ \land σ) \land (η \land ζ)) \leftrightarrow ((ψ \land χ \land η) \land (θ \land σ \land ζ))$
21		3an6	$⊢ ((ψ \land θ) \land (η \land σ) \land (χ \land ζ)) \leftrightarrow ((ψ \land η \land χ) \land (θ \land σ \land ζ))$
22	19 20 21	3bitr4i	$⊢ ((ψ \land θ) \land (χ \land σ) \land (η \land ζ)) \leftrightarrow ((ψ \land θ) \land (η \land σ) \land (χ \land ζ))$
23	12 17 22	3bitri	$⊢ ((ψ \land χ) \land (θ \land η) \land (σ \land ζ)) \leftrightarrow ((ψ \land θ) \land (η \land σ) \land (χ \land ζ))$
24	23	anbi2i	$⊢ ((φ \land τ \land ρ) \land ((ψ \land χ) \land (θ \land η) \land (σ \land ζ))) \leftrightarrow ((φ \land τ \land ρ) \land ((ψ \land θ) \land (η \land σ) \land (χ \land ζ)))$
25	6 7 24	3bitri	$⊢ ((φ \land ψ \land χ) \land (θ \land τ \land η) \land (ζ \land σ \land ρ)) \leftrightarrow ((φ \land τ \land ρ) \land ((ψ \land θ) \land (η \land σ) \land (χ \land ζ)))$

Metamath Proof Explorer

Theorem an33reanOLD

Proof