Theorem andi 837

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

Assertion

Ref	Expression
andi	⊢ ((φ ∧ (ψ ∨ χ)) ↔ ((φ ∧ ψ) ∨ (φ ∧ χ)))

Proof of Theorem andi

Step	Hyp	Ref	Expression
1		orc 374	. . 3 ⊢ ((φ ∧ ψ) → ((φ ∧ ψ) ∨ (φ ∧ χ)))
2		olc 373	. . 3 ⊢ ((φ ∧ χ) → ((φ ∧ ψ) ∨ (φ ∧ χ)))
3	1, 2	jaodan 760	. 2 ⊢ ((φ ∧ (ψ ∨ χ)) → ((φ ∧ ψ) ∨ (φ ∧ χ)))
4		orc 374	. . . 4 ⊢ (ψ → (ψ ∨ χ))
5	4	anim2i 552	. . 3 ⊢ ((φ ∧ ψ) → (φ ∧ (ψ ∨ χ)))
6		olc 373	. . . 4 ⊢ (χ → (ψ ∨ χ))
7	6	anim2i 552	. . 3 ⊢ ((φ ∧ χ) → (φ ∧ (ψ ∨ χ)))
8	5, 7	jaoi 368	. 2 ⊢ (((φ ∧ ψ) ∨ (φ ∧ χ)) → (φ ∧ (ψ ∨ χ)))
9	3, 8	impbii 180	1 ⊢ ((φ ∧ (ψ ∨ χ)) ↔ ((φ ∧ ψ) ∨ (φ ∧ χ)))

This proof depends on syntax axioms:   ↔ wb 176   ∨ wo 357   ∧ wa 358

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

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

This theorem is used by:  andir  838  anddi  840  indi  3502  indifdir  3512  unrab  3527  unipr  3906  uniun  3911  unopab  4639  xpundi  4833  coundir  5084  imadif  5172  unpreima  5409  nmembers1lem3  6271