Metamath Proof Explorer

Theorem orddi

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

Ref Expression
Assertion orddi ⊢ φ ∧ ψ ∨ χ ∧ θ ↔ φ ∨ χ ∧ φ ∨ θ ∧ ψ ∨ χ ∧ ψ ∨ θ

Proof

Step Hyp Ref Expression
1 ordir ⊢ φ ∧ ψ ∨ χ ∧ θ ↔ φ ∨ χ ∧ θ ∧ ψ ∨ χ ∧ θ
2 ordi ⊢ φ ∨ χ ∧ θ ↔ φ ∨ χ ∧ φ ∨ θ
3 ordi ⊢ ψ ∨ χ ∧ θ ↔ ψ ∨ χ ∧ ψ ∨ θ
4 2 3 anbi12i ⊢ φ ∨ χ ∧ θ ∧ ψ ∨ χ ∧ θ ↔ φ ∨ χ ∧ φ ∨ θ ∧ ψ ∨ χ ∧ ψ ∨ θ
5 1 4 bitri ⊢ φ ∧ ψ ∨ χ ∧ θ ↔ φ ∨ χ ∧ φ ∨ θ ∧ ψ ∨ χ ∧ ψ ∨ θ