Theorem mulassd 11159

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   · cmul 11034

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

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

This theorem is referenced by:  recex  11773  mulcand  11774  receu  11786  divmulasscom  11824  divdivdiv  11847  divmuleq  11851  conjmul  11863  modmul1  13877  moddi  13892  expadd  14057  mulbinom2  14176  binom3  14177  digit1  14190  discr1  14192  discr  14193  faclbnd  14243  faclbnd6  14252  bcm1k  14268  bcp1nk  14270  crre  15067  remullem  15081  amgm2  15323  iseraltlem2  15636  iseraltlem3  15637  binomlem  15785  climcndslem2  15806  pwdif  15824  geo2sum  15829  mertenslem1  15840  clim2prod  15844  fallrisefac  15981  binomfallfaclem2  15996  bpolydiflem  16010  bpoly4  16015  sinadd  16122  tanadd  16125  pwp1fsum  16351  bezoutlem3  16501  dvdsmulgcd  16516  qredeq  16617  pcaddlem  16850  prmpwdvds  16866  ablfacrp  20034  nmoco  24712  cph2ass  25190  cphipval2  25218  csbren  25376  minveclem2  25403  uniioombllem5  25564  itg1mulc  25681  mbfi1fseqlem5  25696  itgconst  25796  itgmulc2  25811  dvexp  25930  dvply1  26260  elqaalem3  26298  aalioulem1  26309  aaliou3lem2  26320  dvtaylp  26347  dvradcnv  26399  pserdvlem2  26406  tangtx  26482  tanregt0  26516  tanarg  26596  logcnlem4  26622  cxpmul  26665  dvcxp1  26717  dvcncxp1  26720  root1eq1  26732  heron  26815  quad2  26816  dcubic1lem  26820  dcubic1  26822  cubic2  26825  binom4  26827  dquartlem1  26828  dquartlem2  26829  dquart  26830  quart1lem  26832  quart1  26833  quartlem1  26834  efiasin  26865  asinsinlem  26868  asinsin  26869  efiatan  26889  efiatan2  26894  2efiatan  26895  atantan  26900  atanbndlem  26902  atans2  26908  atantayl  26914  log2cnv  26921  log2tlbnd  26922  ftalem1  27050  ftalem5  27054  basellem3  27060  basellem5  27062  basellem8  27065  chtub  27189  perfectlem1  27206  perfectlem2  27207  perfect  27208  bcmono  27254  bclbnd  27257  bposlem9  27269  lgsneg  27298  gausslemma2dlem6  27349  lgseisenlem1  27352  lgseisenlem2  27353  lgseisenlem3  27354  lgseisenlem4  27355  lgsquad2lem1  27361  lgsquad3  27364  2lgslem3a  27373  2lgslem3b  27374  2lgslem3c  27375  2lgslem3d  27376  2lgsoddprmlem2  27386  2sqlem3  27397  chto1ub  27453  rplogsumlem1  27461  dchrmusum2  27471  dchrvmasum2lem  27473  dchrvmasumlem2  27475  dchrvmasumiflem2  27479  dchrisum0lem1  27493  dchrisum0lem2  27495  mulog2sumlem2  27512  chpdifbndlem1  27530  selberg3lem1  27534  selberg4lem1  27537  selberg34r  27548  pntrlog2bndlem3  27556  pntrlog2bndlem5  27558  pntrlog2bndlem6  27560  pntlemh  27576  pntlemr  27579  pntlemf  27582  pntlemk  27583  pntlemo  27584  colinearalglem4  28992  axpasch  29024  axcontlem2  29048  axcontlem4  29050  axcontlem7  29053  axcontlem8  29054  ipasslem4  30920  minvecolem2  30961  his35  31174  leopnmid  32224  quad3d  32837  zringfrac  33629  ccfldsrarelvec  33831  constrrtll  33891  constrrtlc1  33892  constrrtcclem  33894  constrrtcc  33895  cos9thpiminplylem2  33943  oddpwdc  34514  prodfzo03  34763  itgexpif  34766  breprexplemc  34792  circlemeth  34800  hgt750lemg  34814  hgt750lemb  34816  hgt750leme  34818  subfacval2  35385  subfaclim  35386  circum  35872  faclimlem1  35941  faclimlem3  35943  faclim2  35946  unbdqndv2lem1  36785  knoppndvlem2  36789  knoppndvlem7  36794  knoppndvlem11  36798  knoppndvlem12  36799  knoppndvlem14  36801  knoppndvlem18  36805  itgmulc2nc  38023  areacirclem1  38043  areacirclem4  38046  bfplem1  38157  lcmineqlem1  42482  lcmineqlem5  42486  lcmineqlem10  42491  lcmineqlem12  42493  lcmineqlem18  42499  lcmineqlem20  42501  dvrelogpow2b  42521  aks4d1p1p7  42527  primrootscoprmpow  42552  2np3bcnp1  42597  remulcan2d  42709  remul02  42851  remul01  42853  sn-it0e0  42862  remulinvcom  42879  remullid  42880  sn-mullid  42882  remulcand  42885  rediveud  42889  redivrec2d  42906  rediv23d  42907  sn-0tie0  42910  sn-mul02  42911  mulgt0b1d  42931  mulgt0b2d  42937  mullt0b1d  42942  sn-itrere  42947  sn-retire  42948  flt4lem5e  43103  flt4lem5f  43104  fltnlta  43110  cu3addd  43127  3cubeslem2  43131  3cubeslem3l  43132  3cubeslem3r  43133  pellexlem6  43280  rmxluc  43382  rmyluc2  43384  rmydbl  43386  jm2.18  43434  jm2.23  43442  jm2.27c  43453  jm3.1lem2  43464  proot1ex  43642  sqrtcval  44086  sqrtcval2  44087  int-mulassocd  44622  binomcxplemnotnn0  44801  mul13d  45731  fmul01lt1lem1  46032  fmul01lt1lem2  46033  coskpi2  46312  cosknegpi  46315  dvnxpaek  46388  dvmptfprodlem  46390  dvnprodlem2  46393  itgsinexplem1  46400  stoweidlem26  46472  wallispilem5  46515  wallispi  46516  wallispi2lem1  46517  wallispi2lem2  46518  stirlinglem3  46522  stirlinglem10  46529  stirlinglem15  46534  dirkertrigeqlem1  46544  dirkertrigeqlem2  46545  dirkertrigeqlem3  46546  dirkertrigeq  46547  dirkercncflem2  46550  fourierdlem66  46618  fourierswlem  46676  fouriersw  46677  etransclem23  46703  etransclem25  46705  etransclem46  46726  hoidmvlelem2  47042  sigarls  47303  sharhght  47311  sin3t  47335  cos3t  47336  sin5tlem2  47338  sin5tlem3  47339  sin5tlem4  47340  modmkpkne  47827  fmtnorec4  48024  fmtnoprmfac2lem1  48041  fmtnoprmfac2  48042  fmtnofac2lem  48043  fmtnofac1  48045  lighneallem4a  48083  perfectALTVlem1  48209  perfectALTVlem2  48210  perfectALTV  48211  2zrngmmgm  48740  altgsumbcALT  48841  nn0sumshdiglemB  49108  affinecomb2  49191  itscnhlc0yqe  49247  itschlc0yqe  49248  itsclc0yqsollem1  49250  itsclc0yqsol  49252  itscnhlc0xyqsol  49253  itsclc0xyqsolr  49257  itsclquadb  49264  aacllem  50288