Theorem adddid 11188

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  (class class class)co 7362  ℂcc 11058   + caddc 11063   · cmul 11065

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089

This theorem is referenced by:  addrid  11344  cnegex  11345  addcom  11350  addcomd  11366  subdi  11597  conjmul  11881  cju  12158  flhalf  13745  modcyc  13821  addmodlteq  13861  binom3  14137  sqoddm1div8  14156  bcpasc  14231  hashf1lem2  14367  remim  15014  mulre  15018  readd  15023  remullem  15025  imadd  15031  cjadd  15038  sqreulem  15256  iseraltlem2  15579  o1fsum  15709  binomlem  15725  climcndslem2  15746  binomfallfaclem2  15934  bpoly4  15953  tanval3  16027  sinadd  16057  tanadd  16060  dvdsmulgcd  16447  lcmgcdlem  16493  pythagtriplem1  16699  pcaddlem  16771  prmreclem4  16802  prmreclem6  16804  mul4sqlem  16836  vdwlem3  16866  vdwlem6  16869  vdwlem9  16872  nn0srg  20904  rge0srg  20905  mhppwdeg  21577  icopnfcnv  24342  pcoass  24424  cphipval2  24642  minveclem2  24827  pjthlem1  24838  ovolunlem1a  24897  ovolscalem1  24914  itgcnlem  25191  itgadd  25226  itgmulc2  25235  itgsplit  25237  aaliou3lem2  25740  abelthlem7  25834  tangtx  25899  efgh  25934  tanarg  26011  logcnlem4  26037  mulcxp  26077  cxpmul2  26081  heron  26225  quad2  26226  dcubic1lem  26230  dcubic2  26231  mcubic  26234  binom4  26237  quart1  26243  atanlogsublem  26302  2efiatan  26305  lgamgulmlem3  26417  basellem2  26468  basellem3  26469  basellem8  26474  chtub  26597  bposlem9  26677  lgseisenlem2  26761  2lgsoddprmlem2  26794  2sqlem4  26806  2sqlem8  26811  dchrisumlem1  26874  dchrvmasum2if  26882  dchrisum0re  26898  mulog2sumlem1  26919  selberglem1  26930  selberglem2  26931  selberg  26933  selberg2  26936  chpdifbndlem1  26938  selberg3lem1  26942  selberg4  26946  pntsval2  26961  pntibndlem2  26976  pntlemr  26987  pntlemf  26990  pntlemo  26992  ostth2lem2  27019  ostth2lem3  27020  brbtwn2  27917  axsegconlem9  27937  axpasch  27953  axeuclidlem  27974  axcontlem2  27977  axcontlem4  27979  axcontlem7  27982  axcontlem8  27983  finsumvtxdg2ssteplem4  28559  ipasslem2  29837  minvecolem2  29880  pjhthlem1  30396  wrdt2ind  31877  ccfldsrarelvec  32442  circlemeth  33342  subfacval2  33868  subfaclim  33869  faclimlem1  34402  itgaddnc  36211  itgmulc2nc  36219  dvasin  36235  2np3bcnp1  40625  nnadddir  40844  nnmul1com  40845  nnmulcom  40846  resubdi  40923  sn-negex12  40943  sn-mul01  40952  sn-mullid  40962  sn-0tie0  40966  sn-mul02  40967  renegmulnnass  40980  cnreeu  40995  fltmul  41031  cu3addd  41061  3cubeslem3l  41067  3cubeslem3r  41068  pellexlem6  41215  pell1234qrmulcl  41236  rmxyadd  41303  jm2.25  41381  relexpmulnn  42103  binomcxplemnotnn0  42758  sumnnodd  43991  dvnmul  44304  stoweidlem13  44374  wallispilem4  44429  wallispi2lem1  44432  wallispi2lem2  44433  stirlinglem1  44435  stirlinglem6  44440  stirlinglem7  44441  stirlinglem8  44442  stirlinglem10  44444  dirkerper  44457  dirkertrigeqlem1  44459  dirkertrigeqlem2  44460  dirkertrigeqlem3  44461  fourierdlem83  44550  hoidmvlelem2  44957  hspmbllem1  44987  smfmullem1  45152  deccarry  45663  fmtnorec4  45861  mod42tp1mod8  45914  lighneallem3  45919  opoeALTV  45995  opeoALTV  45996  2zlidl  46352  2zrngamgm  46357  altgsumbcALT  46549  itcovalpclem2  46877  ackval2  46888  affinecomb2  46909  itscnhlc0yqe  46965  itsclc0yqsollem1  46968  itsclc0yqsol  46970  itscnhlc0xyqsol  46971  itsclc0xyqsolr  46975  itscnhlinecirc02plem1  46988