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 865	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
2		olc 866	. . 3 ⊢ ((𝜑 ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
3	1, 2	jaodan 955	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))
4		orc 865	. . . 4 ⊢ (𝜓 → (𝜓 ∨ 𝜒))
5	4	anim2i 615	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
6		olc 866	. . . 4 ⊢ (𝜒 → (𝜓 ∨ 𝜒))
7	6	anim2i 615	. . 3 ⊢ ((𝜑 ∧ 𝜒) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
8	5, 7	jaoi 855	. 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∨ 𝜒)))
9	3, 8	impbii 208	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜑 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 394   ∨ wo 845

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 206  df-an 395  df-or 846

This theorem is referenced by:  andir  1006  anddi  1008  cadan  1602  indi  4272  indifdirOLD  4284  unrab  4304  uniprOLD  4927  uniun  4934  unopab  5231  xpundi  5746  difxp  6170  coundir  6254  imadif  6638  unpreima  7071  soseq  8164  tpostpos  8252  elznn0nn  12605  faclbnd4lem4  14291  opsrtoslem1  22021  mbfmax  25622  fta1glem2  26148  ofmulrt  26261  lgsquadlem3  27360  nogesgn1o  27652  nosep1o  27660  noinfbnd2lem1  27709  difrab2  32374  ordtconnlem1  33656  ballotlemodife  34248  subfacp1lem6  34926  satf0op  35118  lineunray  35874  wl-ifpimpr  37076  wl-df2-3mintru2  37095  poimirlem30  37254  itg2addnclem2  37276  sticksstones22  41771  lzunuz  42330  diophun  42335  rmydioph  42577  fzunt  43027  fzuntd  43028  fzunt1d  43029  fzuntgd  43030  rp-isfinite6  43090  relexpxpmin  43289  andi3or  43596  clsk1indlem3  43615  simpcntrab  46396  zeoALTV  47147