Metamath Proof Explorer

Theorem ordir

Description: Distributive law for disjunction. (Contributed by NM, 12-Aug-1994)

Ref Expression
Assertion ordir ⊢ φ ∧ ψ ∨ χ ↔ φ ∨ χ ∧ ψ ∨ χ

Proof

Step Hyp Ref Expression
1 ordi ⊢ χ ∨ φ ∧ ψ ↔ χ ∨ φ ∧ χ ∨ ψ
2 orcom ⊢ φ ∧ ψ ∨ χ ↔ χ ∨ φ ∧ ψ
3 orcom ⊢ φ ∨ χ ↔ χ ∨ φ
4 orcom ⊢ ψ ∨ χ ↔ χ ∨ ψ
5 3 4 anbi12i ⊢ φ ∨ χ ∧ ψ ∨ χ ↔ χ ∨ φ ∧ χ ∨ ψ
6 1 2 5 3bitr4i ⊢ φ ∧ ψ ∨ χ ↔ φ ∨ χ ∧ ψ ∨ χ