Theorem adddid 11261

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 11217	. 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 7417  ℂcc 11126   + caddc 11131   · cmul 11133

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

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

This theorem is used by:  addrid  11418  cnegex  11419  addcom  11424  addcomd  11440  subdi  11675  conjmul  11960  cju  12242  nnadddir  12320  nnmul1com  12321  nnmulcom  12322  flhalf  13895  modcyc  13971  addmodlteq  14014  binom3  14292  sqoddm1div8  14311  bcpasc  14389  hashf1lem2  14525  remim  15208  mulre  15212  readd  15217  remullem  15219  imadd  15225  cjadd  15232  sqreulem  15451  iseraltlem2  15774  o1fsum  15904  binomlem  15922  climcndslem2  15943  binomfallfaclem2  16132  bpoly4  16151  tanval3  16228  sinadd  16258  tanadd  16261  dvdsmulgcd  16652  lcmgcdlem  16702  pythagtriplem1  16914  pcaddlem  16986  prmreclem4  17017  prmreclem6  17019  mul4sqlem  17051  vdwlem3  17081  vdwlem6  17084  vdwlem9  17087  nn0srg  21656  rge0srg  21657  mhppwdeg  22384  icopnfcnv  25176  pcoass  25258  cphipval2  25475  minveclem2  25660  pjthlem1  25671  ovolunlem1a  25730  ovolscalem1  25747  itgcnlem  26024  itgadd  26059  itgmulc2  26068  itgsplit  26070  aaliou3lem2  26586  abelthlem7  26681  tangtx  26750  efgh  26786  tanarg  26864  logcnlem4  26890  mulcxp  26930  cxpmul2  26934  heron  27083  quad2  27084  dcubic1lem  27088  dcubic2  27089  mcubic  27092  binom4  27095  quart1  27101  atanlogsublem  27160  2efiatan  27163  lgamgulmlem3  27275  basellem2  27326  basellem3  27327  basellem8  27332  chtub  27456  bposlem9  27536  lgseisenlem2  27620  2lgsoddprmlem2  27653  2sqlem4  27665  2sqlem8  27670  dchrisumlem1  27733  dchrvmasum2if  27741  dchrisum0re  27757  mulog2sumlem1  27778  selberglem1  27789  selberglem2  27790  selberg  27792  selberg2  27795  chpdifbndlem1  27797  selberg3lem1  27801  selberg4  27805  pntsval2  27820  pntibndlem2  27835  pntlemr  27846  pntlemf  27849  pntlemo  27851  ostth2lem2  27878  ostth2lem3  27879  brbtwn2  29370  axsegconlem9  29390  axpasch  29406  axeuclidlem  29427  axcontlem2  29430  axcontlem4  29432  axcontlem7  29435  axcontlem8  29436  finsumvtxdg2ssteplem4  30016  ipasslem2  31321  minvecolem2  31364  pjhthlem1  31880  wrdt2ind  33403  ccfldsrarelvec  34189  constrrtcclem  34252  constrremulcl  34285  constrrecl  34287  circlemeth  35156  subfacval2  35774  subfaclim  35775  faclimlem1  36330  itgaddnc  38437  itgmulc2nc  38445  dvasin  38461  posbezout  42974  2np3bcnp1  43018  quadfac  43079  sumcubes  43196  resubdi  43279  sn-negex12  43300  sn-mul01  43309  sn-mullid  43319  redivdird  43345  sn-0tie0  43347  sn-mul02  43348  renegmulnnass  43361  cnreeu  43386  fltmul  43489  cu3addd  43534  3cubeslem3l  43539  3cubeslem3r  43540  pellexlem6  43683  pell1234qrmulcl  43704  rmxyadd  43770  jm2.25  43848  relexpmulnn  44557  binomcxplemnotnn0  45188  sumnnodd  46468  dvnmul  46779  stoweidlem13  46849  wallispilem4  46904  wallispi2lem1  46907  wallispi2lem2  46908  stirlinglem1  46910  stirlinglem6  46915  stirlinglem7  46916  stirlinglem8  46917  stirlinglem10  46919  dirkerper  46932  dirkertrigeqlem1  46934  dirkertrigeqlem2  46935  dirkertrigeqlem3  46936  fourierdlem83  47025  hoidmvlelem2  47432  hspmbllem1  47462  smfmullem1  47627  sin5tlem4  47748  deccarry  48207  fmtnorec4  48460  mod42tp1mod8  48513  lighneallem3  48518  opoeALTV  48607  opeoALTV  48608  2zlidl  49163  2zrngamgm  49168  altgsumbcALT  49291  itcovalpclem2  49609  ackval2  49620  affinecomb2  49641  itscnhlc0yqe  49697  itsclc0yqsollem1  49700  itsclc0yqsol  49702  itscnhlc0xyqsol  49703  itsclc0xyqsolr  49707  itscnhlinecirc02plem1  49720