Theorem mulassd 11167

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  (class class class)co 7368  ℂcc 11036   · cmul 11043

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

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

This theorem is referenced by:  recex  11781  mulcand  11782  receu  11794  divmulasscom  11832  divdivdiv  11854  divmuleq  11858  conjmul  11870  modmul1  13859  moddi  13874  expadd  14039  mulbinom2  14158  binom3  14159  digit1  14172  discr1  14174  discr  14175  faclbnd  14225  faclbnd6  14234  bcm1k  14250  bcp1nk  14252  crre  15049  remullem  15063  amgm2  15305  iseraltlem2  15618  iseraltlem3  15619  binomlem  15764  climcndslem2  15785  pwdif  15803  geo2sum  15808  mertenslem1  15819  clim2prod  15823  fallrisefac  15960  binomfallfaclem2  15975  bpolydiflem  15989  bpoly4  15994  sinadd  16101  tanadd  16104  pwp1fsum  16330  bezoutlem3  16480  dvdsmulgcd  16495  qredeq  16596  pcaddlem  16828  prmpwdvds  16844  ablfacrp  20009  nmoco  24693  cph2ass  25181  cphipval2  25209  csbren  25367  minveclem2  25394  uniioombllem5  25556  itg1mulc  25673  mbfi1fseqlem5  25688  itgconst  25788  itgmulc2  25803  dvexp  25925  dvply1  26259  elqaalem3  26297  aalioulem1  26308  aaliou3lem2  26319  dvtaylp  26346  dvradcnv  26398  pserdvlem2  26406  tangtx  26482  tanregt0  26516  tanarg  26596  logcnlem4  26622  cxpmul  26665  dvcxp1  26717  dvcncxp1  26720  root1eq1  26733  heron  26816  quad2  26817  dcubic1lem  26821  dcubic1  26823  cubic2  26826  binom4  26828  dquartlem1  26829  dquartlem2  26830  dquart  26831  quart1lem  26833  quart1  26834  quartlem1  26835  efiasin  26866  asinsinlem  26869  asinsin  26870  efiatan  26890  efiatan2  26895  2efiatan  26896  atantan  26901  atanbndlem  26903  atans2  26909  atantayl  26915  log2cnv  26922  log2tlbnd  26923  ftalem1  27051  ftalem5  27055  basellem3  27061  basellem5  27063  basellem8  27066  chtub  27191  perfectlem1  27208  perfectlem2  27209  perfect  27210  bcmono  27256  bclbnd  27259  bposlem9  27271  lgsneg  27300  gausslemma2dlem6  27351  lgseisenlem1  27354  lgseisenlem2  27355  lgseisenlem3  27356  lgseisenlem4  27357  lgsquad2lem1  27363  lgsquad3  27366  2lgslem3a  27375  2lgslem3b  27376  2lgslem3c  27377  2lgslem3d  27378  2lgsoddprmlem2  27388  2sqlem3  27399  chto1ub  27455  rplogsumlem1  27463  dchrmusum2  27473  dchrvmasum2lem  27475  dchrvmasumlem2  27477  dchrvmasumiflem2  27481  dchrisum0lem1  27495  dchrisum0lem2  27497  mulog2sumlem2  27514  chpdifbndlem1  27532  selberg3lem1  27536  selberg4lem1  27539  selberg34r  27550  pntrlog2bndlem3  27558  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntlemh  27578  pntlemr  27581  pntlemf  27584  pntlemk  27585  pntlemo  27586  colinearalglem4  28994  axpasch  29026  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  axcontlem8  29056  ipasslem4  30921  minvecolem2  30962  his35  31175  leopnmid  32225  quad3d  32839  zringfrac  33646  ccfldsrarelvec  33848  constrrtll  33908  constrrtlc1  33909  constrrtcclem  33911  constrrtcc  33912  cos9thpiminplylem2  33960  oddpwdc  34531  prodfzo03  34780  itgexpif  34783  breprexplemc  34809  circlemeth  34817  hgt750lemg  34831  hgt750lemb  34833  hgt750leme  34835  subfacval2  35400  subfaclim  35401  circum  35887  faclimlem1  35956  faclimlem3  35958  faclim2  35961  unbdqndv2lem1  36728  knoppndvlem2  36732  knoppndvlem7  36737  knoppndvlem11  36741  knoppndvlem12  36742  knoppndvlem14  36744  knoppndvlem18  36748  itgmulc2nc  37933  areacirclem1  37953  areacirclem4  37956  bfplem1  38067  lcmineqlem1  42393  lcmineqlem5  42397  lcmineqlem10  42402  lcmineqlem12  42404  lcmineqlem18  42410  lcmineqlem20  42412  dvrelogpow2b  42432  aks4d1p1p7  42438  primrootscoprmpow  42463  2np3bcnp1  42508  remulcan2d  42621  remul02  42769  remul01  42771  sn-it0e0  42780  remulinvcom  42797  remullid  42798  sn-mullid  42800  remulcand  42803  rediveud  42807  sn-0tie0  42815  sn-mul02  42816  mulgt0b1d  42836  mulgt0b2d  42842  mullt0b1d  42847  sn-itrere  42852  sn-retire  42853  flt4lem5e  43008  flt4lem5f  43009  fltnlta  43015  cu3addd  43032  3cubeslem2  43036  3cubeslem3l  43037  3cubeslem3r  43038  pellexlem6  43185  rmxluc  43287  rmyluc2  43289  rmydbl  43291  jm2.18  43339  jm2.23  43347  jm2.27c  43358  jm3.1lem2  43369  proot1ex  43547  sqrtcval  43991  sqrtcval2  43992  int-mulassocd  44527  binomcxplemnotnn0  44706  mul13d  45636  fmul01lt1lem1  45938  fmul01lt1lem2  45939  coskpi2  46218  cosknegpi  46221  dvnxpaek  46294  dvmptfprodlem  46296  dvnprodlem2  46299  itgsinexplem1  46306  stoweidlem26  46378  wallispilem5  46421  wallispi  46422  wallispi2lem1  46423  wallispi2lem2  46424  stirlinglem3  46428  stirlinglem10  46435  stirlinglem15  46440  dirkertrigeqlem1  46450  dirkertrigeqlem2  46451  dirkertrigeqlem3  46452  dirkertrigeq  46453  dirkercncflem2  46456  fourierdlem66  46524  fourierswlem  46582  fouriersw  46583  etransclem23  46609  etransclem25  46611  etransclem46  46632  hoidmvlelem2  46948  sigarls  47209  sharhght  47217  modmkpkne  47715  fmtnorec4  47903  fmtnoprmfac2lem1  47920  fmtnoprmfac2  47921  fmtnofac2lem  47922  fmtnofac1  47924  lighneallem4a  47962  perfectALTVlem1  48075  perfectALTVlem2  48076  perfectALTV  48077  2zrngmmgm  48606  altgsumbcALT  48707  nn0sumshdiglemB  48974  affinecomb2  49057  itscnhlc0yqe  49113  itschlc0yqe  49114  itsclc0yqsollem1  49116  itsclc0yqsol  49118  itscnhlc0xyqsol  49119  itsclc0xyqsolr  49123  itsclquadb  49130  aacllem  50154