Theorem andi 1005

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.)

Assertion

Ref	Expression
andi	⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Proof of Theorem andi

Step	Hyp	Ref	Expression
1		orc 864	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 865	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 955	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 864	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 619	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 865	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 619	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 854	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 212	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 209   ∧ wa 399   ∨ wo 844

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 210  df-an 400  df-or 845

This theorem is referenced by:  andir  1006  anddi  1008  cadan  1611  indi  4200  indifdir  4210  unrab  4226  unipr  4817  uniun  4823  unopab  5109  xpundi  5584  difxp  5988  coundir  6068  imadif  6408  unpreima  6810  tpostpos  7895  elznn0nn  11983  faclbnd4lem4  13652  opsrtoslem1  20723  mbfmax  24253  fta1glem2  24767  ofmulrt  24878  lgsquadlem3  25966  difrab2  30268  ordtconnlem1  31277  ballotlemodife  31865  subfacp1lem6  32545  satf0op  32737  soseq  33209  nosep1o  33299  lineunray  33721  wl-ifpimpr  34883  wl-df2-3mintru2  34902  poimirlem30  35087  itg2addnclem2  35109  lzunuz  39709  diophun  39714  rmydioph  39955  rp-isfinite6  40226  relexpxpmin  40418  andi3or  40725  clsk1indlem3  40746  simpcntrab  43484  zeoALTV  44188