Metamath Proof Explorer

Theorem 3or6

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

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

Proof

Step Hyp Ref Expression
1 or4 ⊢ φ ∨ χ ∨ τ ∨ ψ ∨ θ ∨ η ↔ φ ∨ χ ∨ ψ ∨ θ ∨ τ ∨ η
2 or4 ⊢ φ ∨ χ ∨ ψ ∨ θ ↔ φ ∨ ψ ∨ χ ∨ θ
3 2 orbi1i ⊢ φ ∨ χ ∨ ψ ∨ θ ∨ τ ∨ η ↔ φ ∨ ψ ∨ χ ∨ θ ∨ τ ∨ η
4 1 3 bitr2i ⊢ φ ∨ ψ ∨ χ ∨ θ ∨ τ ∨ η ↔ φ ∨ χ ∨ τ ∨ ψ ∨ θ ∨ η
5 df-3or ⊢ φ ∨ ψ ∨ χ ∨ θ ∨ τ ∨ η ↔ φ ∨ ψ ∨ χ ∨ θ ∨ τ ∨ η
6 df-3or ⊢ φ ∨ χ ∨ τ ↔ φ ∨ χ ∨ τ
7 df-3or ⊢ ψ ∨ θ ∨ η ↔ ψ ∨ θ ∨ η
8 6 7 orbi12i ⊢ φ ∨ χ ∨ τ ∨ ψ ∨ θ ∨ η ↔ φ ∨ χ ∨ τ ∨ ψ ∨ θ ∨ η
9 4 5 8 3bitr4i ⊢ φ ∨ ψ ∨ χ ∨ θ ∨ τ ∨ η ↔ φ ∨ χ ∨ τ ∨ ψ ∨ θ ∨ η