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