Metamath Proof Explorer

Theorem orordir

Description: Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995)

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

Proof

Step Hyp Ref Expression
1 oridm ⊢ χ ∨ χ ↔ χ
2 1 orbi2i ⊢ φ ∨ ψ ∨ χ ∨ χ ↔ φ ∨ ψ ∨ χ
3 or4 ⊢ φ ∨ ψ ∨ χ ∨ χ ↔ φ ∨ χ ∨ ψ ∨ χ
4 2 3 bitr3i ⊢ φ ∨ ψ ∨ χ ↔ φ ∨ χ ∨ ψ ∨ χ