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