Metamath Proof Explorer

Theorem andi

Description: Distributive law for conjunction. Theorem *4.4 of WhiteheadRussell p. 118. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 5-Jan-2013)

Ref Expression
Assertion andi ⊢ φ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ φ ∧ χ

Proof

Step Hyp Ref Expression
1 orc ⊢ φ ∧ ψ → φ ∧ ψ ∨ φ ∧ χ
2 olc ⊢ φ ∧ χ → φ ∧ ψ ∨ φ ∧ χ
3 1 2 jaodan ⊢ φ ∧ ψ ∨ χ → φ ∧ ψ ∨ φ ∧ χ
4 orc ⊢ ψ → ψ ∨ χ
5 4 anim2i ⊢ φ ∧ ψ → φ ∧ ψ ∨ χ
6 olc ⊢ χ → ψ ∨ χ
7 6 anim2i ⊢ φ ∧ χ → φ ∧ ψ ∨ χ
8 5 7 jaoi ⊢ φ ∧ ψ ∨ φ ∧ χ → φ ∧ ψ ∨ χ
9 3 8 impbii ⊢ φ ∧ ψ ∨ χ ↔ φ ∧ ψ ∨ φ ∧ χ