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