Theorem adddid 9943

Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addassd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
adddid	⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Proof of Theorem adddid

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		adddi 9904	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1318	1 ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   + caddc 9818   · cmul 9820

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9882

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  addid1  10095  cnegex  10096  addcom  10101  addcomd  10117  subdi  10342  conjmul  10621  cju  10893  flhalf  12493  modcyc  12567  addmodlteq  12607  binom3  12847  sqoddm1div8  12890  bcpasc  12970  hashf1lem2  13097  remim  13705  mulre  13709  readd  13714  remullem  13716  imadd  13722  cjadd  13729  sqreulem  13947  iseraltlem2  14261  o1fsum  14386  binomlem  14400  climcndslem2  14421  binomfallfaclem2  14610  bpoly4  14629  tanval3  14703  sinadd  14733  tanadd  14736  dvdsmulgcd  15112  lcmgcdlem  15157  pythagtriplem1  15359  pcaddlem  15430  prmreclem4  15461  prmreclem6  15463  mul4sqlem  15495  vdwlem3  15525  vdwlem6  15528  vdwlem9  15531  nn0srg  19635  rge0srg  19636  icopnfcnv  22549  pcoass  22632  cphipval2  22848  minveclem2  23005  pjthlem1  23016  ovolunlem1a  23071  ovolscalem1  23088  itgcnlem  23362  itgadd  23397  itgmulc2  23406  itgsplit  23408  aaliou3lem2  23902  abelthlem7  23996  tangtx  24061  efgh  24091  tanarg  24169  logcnlem4  24191  mulcxp  24231  cxpmul2  24235  heron  24365  quad2  24366  dcubic1lem  24370  dcubic2  24371  mcubic  24374  binom4  24377  quart1  24383  atanlogsublem  24442  2efiatan  24445  lgamgulmlem3  24557  basellem2  24608  basellem3  24609  basellem8  24614  chtub  24737  bposlem9  24817  lgseisenlem2  24901  2lgsoddprmlem2  24934  2sqlem4  24946  2sqlem8  24951  dchrisumlem1  24978  dchrvmasum2if  24986  dchrisum0re  25002  mulog2sumlem1  25023  selberglem1  25034  selberglem2  25035  selberg  25037  selberg2  25040  chpdifbndlem1  25042  selberg3lem1  25046  selberg4  25050  pntsval2  25065  pntibndlem2  25080  pntlemr  25091  pntlemf  25094  pntlemo  25096  ostth2lem2  25123  ostth2lem3  25124  brbtwn2  25585  axsegconlem9  25605  axpasch  25621  axeuclidlem  25642  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  ipasslem2  27071  minvecolem2  27115  pjhthlem1  27634  subfacval2  30423  subfaclim  30424  faclimlem1  30882  itgaddnc  32640  itgmulc2nc  32648  dvasin  32666  pellexlem6  36416  pell1234qrmulcl  36437  rmxyadd  36504  jm2.25  36584  relexpmulnn  37020  binomcxplemnotnn0  37577  sumnnodd  38697  dvnmul  38833  stoweidlem13  38906  wallispilem4  38961  wallispi2lem1  38964  wallispi2lem2  38965  stirlinglem1  38967  stirlinglem6  38972  stirlinglem7  38973  stirlinglem8  38974  stirlinglem10  38976  dirkerper  38989  dirkertrigeqlem1  38991  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  fourierdlem83  39082  hoidmvlelem2  39486  hspmbllem1  39516  smfmullem1  39676  deccarry  39941  fmtnorec4  39999  mod42tp1mod8  40057  lighneallem3  40062  opoeALTV  40132  opeoALTV  40133  2zlidl  41724  2zrngamgm  41729  altgsumbcALT  41924