Theorem adddid 11136

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004   + caddc 11009   · cmul 11011

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  addrid  11293  cnegex  11294  addcom  11299  addcomd  11315  subdi  11550  conjmul  11838  cju  12121  flhalf  13734  modcyc  13810  addmodlteq  13853  binom3  14131  sqoddm1div8  14150  bcpasc  14228  hashf1lem2  14363  remim  15024  mulre  15028  readd  15033  remullem  15035  imadd  15041  cjadd  15048  sqreulem  15267  iseraltlem2  15590  o1fsum  15720  binomlem  15736  climcndslem2  15757  binomfallfaclem2  15947  bpoly4  15966  tanval3  16043  sinadd  16073  tanadd  16076  dvdsmulgcd  16467  lcmgcdlem  16517  pythagtriplem1  16728  pcaddlem  16800  prmreclem4  16831  prmreclem6  16833  mul4sqlem  16865  vdwlem3  16895  vdwlem6  16898  vdwlem9  16901  nn0srg  21375  rge0srg  21376  mhppwdeg  22066  icopnfcnv  24868  pcoass  24952  cphipval2  25169  minveclem2  25354  pjthlem1  25365  ovolunlem1a  25425  ovolscalem1  25442  itgcnlem  25719  itgadd  25754  itgmulc2  25763  itgsplit  25765  aaliou3lem2  26279  abelthlem7  26376  tangtx  26442  efgh  26478  tanarg  26556  logcnlem4  26582  mulcxp  26622  cxpmul2  26626  heron  26776  quad2  26777  dcubic1lem  26781  dcubic2  26782  mcubic  26785  binom4  26788  quart1  26794  atanlogsublem  26853  2efiatan  26856  lgamgulmlem3  26969  basellem2  27020  basellem3  27021  basellem8  27026  chtub  27151  bposlem9  27231  lgseisenlem2  27315  2lgsoddprmlem2  27348  2sqlem4  27360  2sqlem8  27365  dchrisumlem1  27428  dchrvmasum2if  27436  dchrisum0re  27452  mulog2sumlem1  27473  selberglem1  27484  selberglem2  27485  selberg  27487  selberg2  27490  chpdifbndlem1  27492  selberg3lem1  27496  selberg4  27500  pntsval2  27515  pntibndlem2  27530  pntlemr  27541  pntlemf  27544  pntlemo  27546  ostth2lem2  27573  ostth2lem3  27574  brbtwn2  28884  axsegconlem9  28904  axpasch  28920  axeuclidlem  28941  axcontlem2  28944  axcontlem4  28946  axcontlem7  28949  axcontlem8  28950  finsumvtxdg2ssteplem4  29528  ipasslem2  30810  minvecolem2  30853  pjhthlem1  31369  wrdt2ind  32932  ccfldsrarelvec  33682  constrrtcclem  33745  constrremulcl  33778  constrrecl  33780  circlemeth  34651  subfacval2  35229  subfaclim  35230  faclimlem1  35785  itgaddnc  37726  itgmulc2nc  37734  dvasin  37750  posbezout  42139  2np3bcnp1  42183  nnadddir  42309  nnmul1com  42310  nnmulcom  42311  sumcubes  42352  resubdi  42435  sn-negex12  42456  sn-mul01  42465  sn-mullid  42475  sn-0tie0  42490  sn-mul02  42491  renegmulnnass  42504  cnreeu  42529  fltmul  42674  cu3addd  42720  3cubeslem3l  42725  3cubeslem3r  42726  pellexlem6  42873  pell1234qrmulcl  42894  rmxyadd  42960  jm2.25  43038  relexpmulnn  43748  binomcxplemnotnn0  44395  sumnnodd  45676  dvnmul  45987  stoweidlem13  46057  wallispilem4  46112  wallispi2lem1  46115  wallispi2lem2  46116  stirlinglem1  46118  stirlinglem6  46123  stirlinglem7  46124  stirlinglem8  46125  stirlinglem10  46127  dirkerper  46140  dirkertrigeqlem1  46142  dirkertrigeqlem2  46143  dirkertrigeqlem3  46144  fourierdlem83  46233  hoidmvlelem2  46640  hspmbllem1  46670  smfmullem1  46835  deccarry  47348  fmtnorec4  47586  mod42tp1mod8  47639  lighneallem3  47644  opoeALTV  47720  opeoALTV  47721  2zlidl  48277  2zrngamgm  48282  altgsumbcALT  48390  itcovalpclem2  48709  ackval2  48720  affinecomb2  48741  itscnhlc0yqe  48797  itsclc0yqsollem1  48800  itsclc0yqsol  48802  itscnhlc0xyqsol  48803  itsclc0xyqsolr  48807  itscnhlinecirc02plem1  48820