Metamath Proof Explorer

Theorem orordi

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

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

Proof

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