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 ⊢φ∨ψ∨χ∨θ∨τ∨η↔φ∨χ∨τ∨ψ∨θ∨η