Metamath Proof Explorer

Theorem orass

Description: Associative law for disjunction. Theorem *4.33 of WhiteheadRussell p. 118. (Contributed by NM, 5-Aug-1993) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion orass ⊢ φ ∨ ψ ∨ χ ↔ φ ∨ ψ ∨ χ

Proof

Step Hyp Ref Expression
1 orcom ⊢ φ ∨ ψ ∨ χ ↔ χ ∨ φ ∨ ψ
2 or12 ⊢ χ ∨ φ ∨ ψ ↔ φ ∨ χ ∨ ψ
3 orcom ⊢ χ ∨ ψ ↔ ψ ∨ χ
4 3 orbi2i ⊢ φ ∨ χ ∨ ψ ↔ φ ∨ ψ ∨ χ
5 1 2 4 3bitri ⊢ φ ∨ ψ ∨ χ ↔ φ ∨ ψ ∨ χ