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