Theorem an6 906

Description: Rearrangement of 6 conjuncts.

Assertion

Ref	Expression
an6	⊢ (((φ ⋀ ψ ⋀ χ) ⋀ (θ ⋀ τ ⋀ η)) ↔ ((φ ⋀ θ) ⋀ (ψ ⋀ τ) ⋀ (χ ⋀ η)))

Proof of Theorem an6

Step	Hyp	Ref	Expression
1		df-3an 781	. . . 4 ⊢ ((φ ⋀ ψ ⋀ χ) ↔ ((φ ⋀ ψ) ⋀ χ))
2		df-3an 781	. . . 4 ⊢ ((θ ⋀ τ ⋀ η) ↔ ((θ ⋀ τ) ⋀ η))
3	1, 2	anbi12i 485	. . 3 ⊢ (((φ ⋀ ψ ⋀ χ) ⋀ (θ ⋀ τ ⋀ η)) ↔ (((φ ⋀ ψ) ⋀ χ) ⋀ ((θ ⋀ τ) ⋀ η)))
4		an4 509	. . 3 ⊢ ((((φ ⋀ ψ) ⋀ χ) ⋀ ((θ ⋀ τ) ⋀ η)) ↔ (((φ ⋀ ψ) ⋀ (θ ⋀ τ)) ⋀ (χ ⋀ η)))
5		an4 509	. . . 4 ⊢ (((φ ⋀ ψ) ⋀ (θ ⋀ τ)) ↔ ((φ ⋀ θ) ⋀ (ψ ⋀ τ)))
6	5	anbi1i 484	. . 3 ⊢ ((((φ ⋀ ψ) ⋀ (θ ⋀ τ)) ⋀ (χ ⋀ η)) ↔ (((φ ⋀ θ) ⋀ (ψ ⋀ τ)) ⋀ (χ ⋀ η)))
7	3, 4, 6	3bitri 177	. 2 ⊢ (((φ ⋀ ψ ⋀ χ) ⋀ (θ ⋀ τ ⋀ η)) ↔ (((φ ⋀ θ) ⋀ (ψ ⋀ τ)) ⋀ (χ ⋀ η)))
8		df-3an 781	. 2 ⊢ (((φ ⋀ θ) ⋀ (ψ ⋀ τ) ⋀ (χ ⋀ η)) ↔ (((φ ⋀ θ) ⋀ (ψ ⋀ τ)) ⋀ (χ ⋀ η)))
9	7, 8	bitr4i 176	1 ⊢ (((φ ⋀ ψ ⋀ χ) ⋀ (θ ⋀ τ ⋀ η)) ↔ ((φ ⋀ θ) ⋀ (ψ ⋀ τ) ⋀ (χ ⋀ η)))

Syntax hints:   ↔ wb 146   ⋀ wa 223   ⋀ w3a 779

This theorem is referenced by:  abfii4 4579  distrlem3pr 5149  ltdiv2 5901  elfzuzb 6444  efcltlem1 7336  iscau3 7964  iscau4 7966  infi1 10471  ficli 10492  filintf 10601  infi 10606  rcfpfillem4 10613

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 781

Copyright terms: Public domain