Theorem anddi 840

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

Assertion

Ref	Expression
anddi	⊢ (((φ ∨ ψ) ∧ (χ ∨ θ)) ↔ (((φ ∧ χ) ∨ (φ ∧ θ)) ∨ ((ψ ∧ χ) ∨ (ψ ∧ θ))))

Proof of Theorem anddi

Step	Hyp	Ref	Expression
1		andir 838	. 2 ⊢ (((φ ∨ ψ) ∧ (χ ∨ θ)) ↔ ((φ ∧ (χ ∨ θ)) ∨ (ψ ∧ (χ ∨ θ))))
2		andi 837	. . 3 ⊢ ((φ ∧ (χ ∨ θ)) ↔ ((φ ∧ χ) ∨ (φ ∧ θ)))
3		andi 837	. . 3 ⊢ ((ψ ∧ (χ ∨ θ)) ↔ ((ψ ∧ χ) ∨ (ψ ∧ θ)))
4	2, 3	orbi12i 507	. 2 ⊢ (((φ ∧ (χ ∨ θ)) ∨ (ψ ∧ (χ ∨ θ))) ↔ (((φ ∧ χ) ∨ (φ ∧ θ)) ∨ ((ψ ∧ χ) ∨ (ψ ∧ θ))))
5	1, 4	bitri 240	1 ⊢ (((φ ∨ ψ) ∧ (χ ∨ θ)) ↔ (((φ ∧ χ) ∨ (φ ∧ θ)) ∨ ((ψ ∧ χ) ∨ (ψ ∧ θ))))

Syntax hints:   ↔ wb 176   ∨ wo 357   ∧ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360

This theorem is referenced by:  funun  5147