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