Metamath Proof Explorer

Theorem ordi

Description: Distributive law for disjunction. Theorem *4.41 of WhiteheadRussell p. 119. (Contributed by NM, 5-Jan-1993) (Proof shortened by Andrew Salmon, 7-May-2011) (Proof shortened by Wolf Lammen, 28-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 jcab ⊢ ¬ φ → ψ ∧ χ ↔ ¬ φ → ψ ∧ ¬ φ → χ
2 df-or ⊢ φ ∨ ψ ∧ χ ↔ ¬ φ → ψ ∧ χ
3 df-or ⊢ φ ∨ ψ ↔ ¬ φ → ψ
4 df-or ⊢ φ ∨ χ ↔ ¬ φ → χ
5 3 4 anbi12i ⊢ φ ∨ ψ ∧ φ ∨ χ ↔ ¬ φ → ψ ∧ ¬ φ → χ
6 1 2 5 3bitr4i ⊢ φ ∨ ψ ∧ χ ↔ φ ∨ ψ ∧ φ ∨ χ