Theorem adddid 11260

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7416  ℂcc 11125   + caddc 11130   · cmul 11132

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

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  addrid  11417  cnegex  11418  addcom  11423  addcomd  11439  subdi  11674  conjmul  11959  cju  12241  nnadddir  12319  nnmul1com  12320  nnmulcom  12321  flhalf  13893  modcyc  13969  addmodlteq  14012  binom3  14290  sqoddm1div8  14309  bcpasc  14387  hashf1lem2  14523  remim  15206  mulre  15210  readd  15215  remullem  15217  imadd  15223  cjadd  15230  sqreulem  15449  iseraltlem2  15772  o1fsum  15902  binomlem  15920  climcndslem2  15941  binomfallfaclem2  16130  bpoly4  16149  tanval3  16226  sinadd  16256  tanadd  16259  dvdsmulgcd  16650  lcmgcdlem  16700  pythagtriplem1  16912  pcaddlem  16984  prmreclem4  17015  prmreclem6  17017  mul4sqlem  17049  vdwlem3  17079  vdwlem6  17082  vdwlem9  17085  nn0srg  21651  rge0srg  21652  mhppwdeg  22379  icopnfcnv  25171  pcoass  25253  cphipval2  25470  minveclem2  25655  pjthlem1  25666  ovolunlem1a  25725  ovolscalem1  25742  itgcnlem  26019  itgadd  26054  itgmulc2  26063  itgsplit  26065  aaliou3lem2  26576  abelthlem7  26671  tangtx  26740  efgh  26776  tanarg  26854  logcnlem4  26880  mulcxp  26920  cxpmul2  26924  heron  27073  quad2  27074  dcubic1lem  27078  dcubic2  27079  mcubic  27082  binom4  27085  quart1  27091  atanlogsublem  27150  2efiatan  27153  lgamgulmlem3  27265  basellem2  27316  basellem3  27317  basellem8  27322  chtub  27446  bposlem9  27526  lgseisenlem2  27610  2lgsoddprmlem2  27643  2sqlem4  27655  2sqlem8  27660  dchrisumlem1  27723  dchrvmasum2if  27731  dchrisum0re  27747  mulog2sumlem1  27768  selberglem1  27779  selberglem2  27780  selberg  27782  selberg2  27785  chpdifbndlem1  27787  selberg3lem1  27791  selberg4  27795  pntsval2  27810  pntibndlem2  27825  pntlemr  27836  pntlemf  27839  pntlemo  27841  ostth2lem2  27868  ostth2lem3  27869  brbtwn2  29348  axsegconlem9  29368  axpasch  29384  axeuclidlem  29405  axcontlem2  29408  axcontlem4  29410  axcontlem7  29413  axcontlem8  29414  finsumvtxdg2ssteplem4  29994  ipasslem2  31299  minvecolem2  31342  pjhthlem1  31858  wrdt2ind  33382  ccfldsrarelvec  34168  constrrtcclem  34231  constrremulcl  34264  constrrecl  34266  circlemeth  35135  subfacval2  35753  subfaclim  35754  faclimlem1  36309  itgaddnc  38416  itgmulc2nc  38424  dvasin  38440  posbezout  42953  2np3bcnp1  42997  quadfac  43058  sumcubes  43175  resubdi  43258  sn-negex12  43279  sn-mul01  43288  sn-mullid  43298  redivdird  43324  sn-0tie0  43326  sn-mul02  43327  renegmulnnass  43340  cnreeu  43365  fltmul  43468  cu3addd  43513  3cubeslem3l  43518  3cubeslem3r  43519  pellexlem6  43662  pell1234qrmulcl  43683  rmxyadd  43749  jm2.25  43827  relexpmulnn  44536  binomcxplemnotnn0  45167  sumnnodd  46447  dvnmul  46758  stoweidlem13  46828  wallispilem4  46883  wallispi2lem1  46886  wallispi2lem2  46887  stirlinglem1  46889  stirlinglem6  46894  stirlinglem7  46895  stirlinglem8  46896  stirlinglem10  46898  dirkerper  46911  dirkertrigeqlem1  46913  dirkertrigeqlem2  46914  dirkertrigeqlem3  46915  fourierdlem83  47004  hoidmvlelem2  47411  hspmbllem1  47441  smfmullem1  47606  sin5tlem4  47727  deccarry  48186  fmtnorec4  48439  mod42tp1mod8  48492  lighneallem3  48497  opoeALTV  48586  opeoALTV  48587  2zlidl  49142  2zrngamgm  49147  altgsumbcALT  49270  itcovalpclem2  49588  ackval2  49599  affinecomb2  49620  itscnhlc0yqe  49676  itsclc0yqsollem1  49679  itsclc0yqsol  49681  itscnhlc0xyqsol  49682  itsclc0xyqsolr  49686  itscnhlinecirc02plem1  49699