Theorem mulassd 9942

Description: Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addassd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
mulassd	⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Proof of Theorem mulassd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		mulass 9903	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1318	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   · cmul 9820

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  recex  10538  mulcand  10539  receu  10551  divmulasscom  10588  divdivdiv  10605  divmuleq  10609  conjmul  10621  modmul1  12585  moddi  12600  expadd  12764  mulbinom2  12846  binom3  12847  digit1  12860  discr1  12862  discr  12863  faclbnd  12939  faclbnd6  12948  bcm1k  12964  bcp1nk  12966  crre  13702  remullem  13716  amgm2  13957  iseraltlem2  14261  iseraltlem3  14262  binomlem  14400  climcndslem2  14421  geo2sum  14443  mertenslem1  14455  clim2prod  14459  fallrisefac  14595  binomfallfaclem2  14610  bpolydiflem  14624  bpoly4  14629  sinadd  14733  tanadd  14736  pwp1fsum  14952  bezoutlem3  15096  dvdsmulgcd  15112  qredeq  15209  pcaddlem  15430  prmpwdvds  15446  ablfacrp  18288  nmoco  22351  cph2ass  22821  cphipval2  22848  csbren  22990  minveclem2  23005  uniioombllem5  23161  itg1mulc  23277  mbfi1fseqlem5  23292  itgconst  23391  itgmulc2  23406  dvexp  23522  dvply1  23843  elqaalem3  23880  aalioulem1  23891  aaliou3lem2  23902  dvtaylp  23928  dvradcnv  23979  pserdvlem2  23986  tangtx  24061  tanregt0  24089  tanarg  24169  logcnlem4  24191  cxpmul  24234  dvcxp1  24281  dvcncxp1  24284  root1eq1  24296  heron  24365  quad2  24366  dcubic1lem  24370  dcubic1  24372  cubic2  24375  binom4  24377  dquartlem1  24378  dquartlem2  24379  dquart  24380  quart1lem  24382  quart1  24383  quartlem1  24384  efiasin  24415  asinsinlem  24418  asinsin  24419  efiatan  24439  efiatan2  24444  2efiatan  24445  atantan  24450  atanbndlem  24452  atans2  24458  atantayl  24464  log2cnv  24471  log2tlbnd  24472  ftalem1  24599  ftalem5  24603  basellem3  24609  basellem5  24611  basellem8  24614  chtub  24737  perfectlem1  24754  perfectlem2  24755  perfect  24756  bcmono  24802  bclbnd  24805  bposlem9  24817  lgsneg  24846  gausslemma2dlem6  24897  lgseisenlem1  24900  lgseisenlem2  24901  lgseisenlem3  24902  lgseisenlem4  24903  lgsquad2lem1  24909  lgsquad3  24912  2lgslem3a  24921  2lgslem3b  24922  2lgslem3c  24923  2lgslem3d  24924  2lgsoddprmlem2  24934  2sqlem3  24945  chto1ub  24965  rplogsumlem1  24973  dchrmusum2  24983  dchrvmasum2lem  24985  dchrvmasumlem2  24987  dchrvmasumiflem2  24991  dchrisum0lem1  25005  dchrisum0lem2  25007  mulog2sumlem2  25024  chpdifbndlem1  25042  selberg3lem1  25046  selberg4lem1  25049  selberg34r  25060  pntrlog2bndlem3  25068  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntlemh  25088  pntlemr  25091  pntlemf  25094  pntlemk  25095  pntlemo  25096  colinearalglem4  25589  axpasch  25621  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  ipasslem4  27073  minvecolem2  27115  his35  27329  leopnmid  28381  oddpwdc  29743  subfacval2  30423  subfaclim  30424  circum  30822  faclimlem1  30882  faclimlem3  30884  faclim2  30887  unbdqndv2lem1  31670  knoppndvlem2  31674  knoppndvlem7  31679  knoppndvlem11  31683  knoppndvlem12  31684  knoppndvlem14  31686  knoppndvlem18  31690  itgmulc2nc  32648  areacirclem1  32670  areacirclem4  32673  bfplem1  32791  pellexlem6  36416  rmxluc  36519  rmyluc2  36521  rmydbl  36523  jm2.18  36573  jm2.23  36581  jm2.27c  36592  jm3.1lem2  36603  proot1ex  36798  int-mulassocd  37502  binomcxplemnotnn0  37577  mul13d  38432  fmul01lt1lem1  38651  fmul01lt1lem2  38652  coskpi2  38749  cosknegpi  38752  dvnxpaek  38832  dvmptfprodlem  38834  dvnprodlem2  38837  itgsinexplem1  38845  stoweidlem26  38919  wallispilem5  38962  wallispi  38963  wallispi2lem1  38964  wallispi2lem2  38965  stirlinglem3  38969  stirlinglem10  38976  stirlinglem15  38981  dirkertrigeqlem1  38991  dirkertrigeqlem2  38992  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkercncflem2  38997  fourierdlem66  39065  fourierswlem  39123  fouriersw  39124  etransclem23  39150  etransclem25  39152  etransclem46  39173  hoidmvlelem2  39486  sigarls  39695  sharhght  39703  fmtnorec4  39999  fmtnoprmfac2lem1  40016  fmtnoprmfac2  40017  fmtnofac2lem  40018  fmtnofac1  40020  pwdif  40039  lighneallem4a  40063  perfectALTVlem1  40164  perfectALTVlem2  40165  perfectALTV  40166  2zrngmmgm  41736  altgsumbcALT  41924  nn0sumshdiglemB  42212  aacllem  42356