Theorem adddid 11203

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 11159	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1389	1 ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068   + caddc 11073   · cmul 11075

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099

This theorem is referenced by:  addrid  11360  cnegex  11361  addcom  11366  addcomd  11382  subdi  11617  conjmul  11905  cju  12188  nnadddir  12266  nnmul1com  12267  nnmulcom  12268  flhalf  13837  modcyc  13913  addmodlteq  13956  binom3  14234  sqoddm1div8  14253  bcpasc  14331  hashf1lem2  14466  remim  15127  mulre  15131  readd  15136  remullem  15138  imadd  15144  cjadd  15151  sqreulem  15370  iseraltlem2  15693  o1fsum  15824  binomlem  15842  climcndslem2  15863  binomfallfaclem2  16053  bpoly4  16072  tanval3  16149  sinadd  16179  tanadd  16182  dvdsmulgcd  16573  lcmgcdlem  16623  pythagtriplem1  16835  pcaddlem  16907  prmreclem4  16938  prmreclem6  16940  mul4sqlem  16972  vdwlem3  17002  vdwlem6  17005  vdwlem9  17008  nn0srg  21469  rge0srg  21470  mhppwdeg  22195  icopnfcnv  24984  pcoass  25066  cphipval2  25283  minveclem2  25468  pjthlem1  25479  ovolunlem1a  25538  ovolscalem1  25555  itgcnlem  25832  itgadd  25867  itgmulc2  25876  itgsplit  25878  aaliou3lem2  26384  abelthlem7  26478  tangtx  26547  efgh  26583  tanarg  26661  logcnlem4  26687  mulcxp  26727  cxpmul2  26731  heron  26880  quad2  26881  dcubic1lem  26885  dcubic2  26886  mcubic  26889  binom4  26892  quart1  26898  atanlogsublem  26957  2efiatan  26960  lgamgulmlem3  27072  basellem2  27123  basellem3  27124  basellem8  27129  chtub  27253  bposlem9  27333  lgseisenlem2  27417  2lgsoddprmlem2  27450  2sqlem4  27462  2sqlem8  27467  dchrisumlem1  27530  dchrvmasum2if  27538  dchrisum0re  27554  mulog2sumlem1  27575  selberglem1  27586  selberglem2  27587  selberg  27589  selberg2  27592  chpdifbndlem1  27594  selberg3lem1  27598  selberg4  27602  pntsval2  27617  pntibndlem2  27632  pntlemr  27643  pntlemf  27646  pntlemo  27648  ostth2lem2  27675  ostth2lem3  27676  brbtwn2  29052  axsegconlem9  29072  axpasch  29088  axeuclidlem  29109  axcontlem2  29112  axcontlem4  29114  axcontlem7  29117  axcontlem8  29118  finsumvtxdg2ssteplem4  29695  ipasslem2  30981  minvecolem2  31024  pjhthlem1  31540  wrdt2ind  33092  ccfldsrarelvec  33929  constrrtcclem  33992  constrremulcl  34025  constrrecl  34027  circlemeth  34898  subfacval2  35501  subfaclim  35502  faclimlem1  36057  itgaddnc  38143  itgmulc2nc  38151  dvasin  38167  posbezout  42681  2np3bcnp1  42725  sumcubes  42886  resubdi  42969  sn-negex12  42990  sn-mul01  42999  sn-mullid  43009  redivdird  43035  sn-0tie0  43037  sn-mul02  43038  renegmulnnass  43051  cnreeu  43076  fltmul  43181  cu3addd  43226  3cubeslem3l  43231  3cubeslem3r  43232  pellexlem6  43375  pell1234qrmulcl  43396  rmxyadd  43462  jm2.25  43540  relexpmulnn  44249  binomcxplemnotnn0  44896  sumnnodd  46170  dvnmul  46481  stoweidlem13  46551  wallispilem4  46606  wallispi2lem1  46609  wallispi2lem2  46610  stirlinglem1  46612  stirlinglem6  46617  stirlinglem7  46618  stirlinglem8  46619  stirlinglem10  46621  dirkerper  46634  dirkertrigeqlem1  46636  dirkertrigeqlem2  46637  dirkertrigeqlem3  46638  fourierdlem83  46727  hoidmvlelem2  47134  hspmbllem1  47164  smfmullem1  47329  sin5tlem4  47434  deccarry  47869  fmtnorec4  48122  mod42tp1mod8  48175  lighneallem3  48180  opoeALTV  48269  opeoALTV  48270  2zlidl  48826  2zrngamgm  48831  altgsumbcALT  48939  itcovalpclem2  49257  ackval2  49268  affinecomb2  49289  itscnhlc0yqe  49345  itsclc0yqsollem1  49348  itsclc0yqsol  49350  itscnhlc0xyqsol  49351  itsclc0xyqsolr  49355  itscnhlinecirc02plem1  49368