Metamath Proof Explorer

Theorem anddi

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

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

Proof

Step Hyp Ref Expression
1 andir ⊢ φ ∨ ψ ∧ χ ∨ θ ↔ φ ∧ χ ∨ θ ∨ ψ ∧ χ ∨ θ
2 andi ⊢ φ ∧ χ ∨ θ ↔ φ ∧ χ ∨ φ ∧ θ
3 andi ⊢ ψ ∧ χ ∨ θ ↔ ψ ∧ χ ∨ ψ ∧ θ
4 2 3 orbi12i ⊢ φ ∧ χ ∨ θ ∨ ψ ∧ χ ∨ θ ↔ φ ∧ χ ∨ φ ∧ θ ∨ ψ ∧ χ ∨ ψ ∧ θ
5 1 4 bitri ⊢ φ ∨ ψ ∧ χ ∨ θ ↔ φ ∧ χ ∨ φ ∧ θ ∨ ψ ∧ χ ∨ ψ ∧ θ