Theorem mulassd 11202

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  (class class class)co 7392  ℂcc 11068   · cmul 11075

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1099

This theorem is referenced by:  recex  11816  mulcand  11817  receu  11829  divmulasscom  11866  divdivdiv  11889  divmuleq  11893  conjmul  11905  modmul1  13934  moddi  13949  expadd  14114  mulbinom2  14233  binom3  14234  digit1  14247  discr1  14249  discr  14250  faclbnd  14300  faclbnd6  14309  bcm1k  14325  bcp1nk  14327  crre  15124  remullem  15138  amgm2  15380  iseraltlem2  15693  iseraltlem3  15694  binomlem  15842  climcndslem2  15863  pwdif  15881  geo2sum  15886  mertenslem1  15897  clim2prod  15901  fallrisefac  16038  binomfallfaclem2  16053  bpolydiflem  16067  bpoly4  16072  sinadd  16179  tanadd  16182  pwp1fsum  16408  bezoutlem3  16558  dvdsmulgcd  16573  qredeq  16674  pcaddlem  16907  prmpwdvds  16923  ablfacrp  20091  nmoco  24777  cph2ass  25255  cphipval2  25283  csbren  25441  minveclem2  25468  uniioombllem5  25629  itg1mulc  25746  mbfi1fseqlem5  25761  itgconst  25861  itgmulc2  25876  dvexp  25995  dvply1  26325  elqaalem3  26362  aalioulem1  26373  aaliou3lem2  26384  dvtaylp  26410  dvradcnv  26461  pserdvlem2  26468  tangtx  26547  tanregt0  26581  tanarg  26661  logcnlem4  26687  cxpmul  26730  dvcxp1  26782  dvcncxp1  26785  root1eq1  26797  heron  26880  quad2  26881  dcubic1lem  26885  dcubic1  26887  cubic2  26890  binom4  26892  dquartlem1  26893  dquartlem2  26894  dquart  26895  quart1lem  26897  quart1  26898  quartlem1  26899  efiasin  26930  asinsinlem  26933  asinsin  26934  efiatan  26954  efiatan2  26959  2efiatan  26960  atantan  26965  atanbndlem  26967  atans2  26973  atantayl  26979  log2cnv  26986  log2tlbnd  26987  ftalem1  27114  ftalem5  27118  basellem3  27124  basellem5  27126  basellem8  27129  chtub  27253  perfectlem1  27270  perfectlem2  27271  perfect  27272  bcmono  27318  bclbnd  27321  bposlem9  27333  lgsneg  27362  gausslemma2dlem6  27413  lgseisenlem1  27416  lgseisenlem2  27417  lgseisenlem3  27418  lgseisenlem4  27419  lgsquad2lem1  27425  lgsquad3  27428  2lgslem3a  27437  2lgslem3b  27438  2lgslem3c  27439  2lgslem3d  27440  2lgsoddprmlem2  27450  2sqlem3  27461  chto1ub  27517  rplogsumlem1  27525  dchrmusum2  27535  dchrvmasum2lem  27537  dchrvmasumlem2  27539  dchrvmasumiflem2  27543  dchrisum0lem1  27557  dchrisum0lem2  27559  mulog2sumlem2  27576  chpdifbndlem1  27594  selberg3lem1  27598  selberg4lem1  27601  selberg34r  27612  pntrlog2bndlem3  27620  pntrlog2bndlem5  27622  pntrlog2bndlem6  27624  pntlemh  27640  pntlemr  27643  pntlemf  27646  pntlemk  27647  pntlemo  27648  colinearalglem4  29056  axpasch  29088  axcontlem2  29112  axcontlem4  29114  axcontlem7  29117  axcontlem8  29118  ipasslem4  30983  minvecolem2  31024  his35  31237  leopnmid  32287  quad3d  32901  zringfrac  33711  ccfldsrarelvec  33929  constrrtll  33989  constrrtlc1  33990  constrrtcclem  33992  constrrtcc  33993  cos9thpiminplylem2  34041  oddpwdc  34612  prodfzo03  34861  itgexpif  34864  breprexplemc  34890  circlemeth  34898  hgt750lemg  34912  hgt750lemb  34914  hgt750leme  34916  subfacval2  35501  subfaclim  35502  circum  35988  faclimlem1  36057  faclimlem3  36059  faclim2  36062  unbdqndv2lem1  36911  knoppndvlem2  36915  knoppndvlem7  36920  knoppndvlem11  36924  knoppndvlem12  36925  knoppndvlem14  36927  knoppndvlem18  36931  itgmulc2nc  38151  areacirclem1  38171  areacirclem4  38174  bfplem1  38285  lcmineqlem1  42610  lcmineqlem5  42614  lcmineqlem10  42619  lcmineqlem12  42621  lcmineqlem18  42627  lcmineqlem20  42629  dvrelogpow2b  42649  aks4d1p1p7  42655  primrootscoprmpow  42680  2np3bcnp1  42725  remulcan2d  42836  remul02  42978  remul01  42980  sn-it0e0  42989  remulinvcom  43006  remullid  43007  sn-mullid  43009  remulcand  43012  rediveud  43016  redivrec2d  43033  rediv23d  43034  sn-0tie0  43037  sn-mul02  43038  mulgt0b1d  43058  mulgt0b2d  43064  mullt0b1d  43069  sn-itrere  43074  sn-retire  43075  flt4lem5e  43202  flt4lem5f  43203  fltnlta  43209  cu3addd  43226  3cubeslem2  43230  3cubeslem3l  43231  3cubeslem3r  43232  pellexlem6  43375  rmxluc  43477  rmyluc2  43479  rmydbl  43481  jm2.18  43529  jm2.23  43537  jm2.27c  43548  jm3.1lem2  43559  proot1ex  43737  sqrtcval  44181  sqrtcval2  44182  int-mulassocd  44717  binomcxplemnotnn0  44896  mul13d  45823  fmul01lt1lem1  46124  fmul01lt1lem2  46125  coskpi2  46404  cosknegpi  46407  dvnxpaek  46480  dvmptfprodlem  46482  dvnprodlem2  46485  itgsinexplem1  46492  stoweidlem26  46564  wallispilem5  46607  wallispi  46608  wallispi2lem1  46609  wallispi2lem2  46610  stirlinglem3  46614  stirlinglem10  46621  stirlinglem15  46626  dirkertrigeqlem1  46636  dirkertrigeqlem2  46637  dirkertrigeqlem3  46638  dirkertrigeq  46639  dirkercncflem2  46642  fourierdlem66  46710  fourierswlem  46768  fouriersw  46769  etransclem23  46795  etransclem25  46797  etransclem46  46818  hoidmvlelem2  47134  sigarls  47395  sharhght  47403  sin3t  47429  cos3t  47430  sin5tlem2  47432  sin5tlem3  47433  sin5tlem4  47434  modmkpkne  47925  fmtnorec4  48122  fmtnoprmfac2lem1  48139  fmtnoprmfac2  48140  fmtnofac2lem  48141  fmtnofac1  48143  lighneallem4a  48181  perfectALTVlem1  48307  perfectALTVlem2  48308  perfectALTV  48309  2zrngmmgm  48838  altgsumbcALT  48939  nn0sumshdiglemB  49206  affinecomb2  49289  itscnhlc0yqe  49345  itschlc0yqe  49346  itsclc0yqsollem1  49348  itsclc0yqsol  49350  itscnhlc0xyqsol  49351  itsclc0xyqsolr  49355  itsclquadb  49362  aacllem  50386