Theorem 3or6 1263

Description: Analog of or4 514 for triple conjunction. (Contributed by Scott Fenton, 16-Mar-2011.)

Assertion

Ref	Expression
3or6	⊢ (((φ ∨ ψ) ∨ (χ ∨ θ) ∨ (τ ∨ η)) ↔ ((φ ∨ χ ∨ τ) ∨ (ψ ∨ θ ∨ η)))

Proof of Theorem 3or6

Step	Hyp	Ref	Expression
1		or4 514	. . 3 ⊢ ((((φ ∨ χ) ∨ τ) ∨ ((ψ ∨ θ) ∨ η)) ↔ (((φ ∨ χ) ∨ (ψ ∨ θ)) ∨ (τ ∨ η)))
2		or4 514	. . . 4 ⊢ (((φ ∨ χ) ∨ (ψ ∨ θ)) ↔ ((φ ∨ ψ) ∨ (χ ∨ θ)))
3	2	orbi1i 506	. . 3 ⊢ ((((φ ∨ χ) ∨ (ψ ∨ θ)) ∨ (τ ∨ η)) ↔ (((φ ∨ ψ) ∨ (χ ∨ θ)) ∨ (τ ∨ η)))
4	1, 3	bitr2i 241	. 2 ⊢ ((((φ ∨ ψ) ∨ (χ ∨ θ)) ∨ (τ ∨ η)) ↔ (((φ ∨ χ) ∨ τ) ∨ ((ψ ∨ θ) ∨ η)))
5		df-3or 935	. 2 ⊢ (((φ ∨ ψ) ∨ (χ ∨ θ) ∨ (τ ∨ η)) ↔ (((φ ∨ ψ) ∨ (χ ∨ θ)) ∨ (τ ∨ η)))
6		df-3or 935	. . 3 ⊢ ((φ ∨ χ ∨ τ) ↔ ((φ ∨ χ) ∨ τ))
7		df-3or 935	. . 3 ⊢ ((ψ ∨ θ ∨ η) ↔ ((ψ ∨ θ) ∨ η))
8	6, 7	orbi12i 507	. 2 ⊢ (((φ ∨ χ ∨ τ) ∨ (ψ ∨ θ ∨ η)) ↔ (((φ ∨ χ) ∨ τ) ∨ ((ψ ∨ θ) ∨ η)))
9	4, 5, 8	3bitr4i 268	1 ⊢ (((φ ∨ ψ) ∨ (χ ∨ θ) ∨ (τ ∨ η)) ↔ ((φ ∨ χ ∨ τ) ∨ (ψ ∨ θ ∨ η)))

This proof depends on syntax axioms:   ↔ wb 176   ∨ wo 357   ∨ w3o 933

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-or 359  df-3or 935

This theorem is used by: (None)