Theorem mulassd 11313

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179   · cmul 11186

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 11247

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  recex  11929  mulcand  11930  receu  11942  divmulasscom  11979  divdivdiv  11999  divmuleq  12003  conjmul  12015  modmul1  14047  moddi  14062  expadd  14227  mulbinom2  14347  binom3  14348  digit1  14361  discr1  14363  discr  14364  faclbnd  14414  faclbnd6  14423  bcm1k  14439  bcp1nk  14441  crre  15261  remullem  15275  amgm2  15517  iseraltlem2  15830  iseraltlem3  15831  binomlem  15978  climcndslem2  15999  pwdif  16017  geo2sum  16022  mertenslem1  16033  clim2prod  16037  fallrisefac  16172  binomfallfaclem2  16186  bpolydiflem  16200  bpoly4  16205  sinadd  16312  tanadd  16315  pwp1fsum  16541  bezoutlem3  16694  dvdsmulgcd  16710  qredeq  16812  pcaddlem  17046  prmpwdvds  17062  ablfacrp  20262  nmoco  25036  cph2ass  25514  cphipval2  25542  csbren  25700  minveclem2  25727  uniioombllem5  25888  itg1mulc  26005  mbfi1fseqlem5  26020  itgconst  26119  itgmulc2  26134  dvexp  26253  dvply1  26587  elqaalem3  26626  aalioulem1  26641  aaliou3lem2  26652  dvtaylp  26679  dvradcnv  26730  pserdvlem2  26737  tangtx  26816  tanregt0  26849  tanarg  26929  logcnlem4  26955  cxpmul  26998  dvcxp1  27050  dvcncxp1  27053  root1eq1  27065  heron  27148  quad2  27149  dcubic1lem  27153  dcubic1  27155  cubic2  27158  binom4  27160  dquartlem1  27161  dquartlem2  27162  dquart  27163  quart1lem  27165  quart1  27166  quartlem1  27167  efiasin  27198  asinsinlem  27201  asinsin  27202  efiatan  27222  efiatan2  27227  2efiatan  27228  atantan  27233  atanbndlem  27235  atans2  27241  atantayl  27247  log2cnv  27254  log2tlbnd  27255  ftalem1  27382  ftalem5  27386  basellem3  27392  basellem5  27394  basellem8  27397  chtub  27521  perfectlem1  27538  perfectlem2  27539  perfect  27540  bcmono  27586  bclbnd  27589  bposlem9  27601  lgsneg  27630  gausslemma2dlem6  27681  lgseisenlem1  27684  lgseisenlem2  27685  lgseisenlem3  27686  lgseisenlem4  27687  lgsquad2lem1  27693  lgsquad3  27696  2lgslem3a  27705  2lgslem3b  27706  2lgslem3c  27707  2lgslem3d  27708  2lgsoddprmlem2  27718  2sqlem3  27729  chto1ub  27785  rplogsumlem1  27793  dchrmusum2  27803  dchrvmasum2lem  27805  dchrvmasumlem2  27807  dchrvmasumiflem2  27811  dchrisum0lem1  27825  dchrisum0lem2  27827  mulog2sumlem2  27844  chpdifbndlem1  27862  selberg3lem1  27866  selberg4lem1  27869  selberg34r  27880  pntrlog2bndlem3  27888  pntrlog2bndlem5  27890  pntrlog2bndlem6  27892  pntlemh  27908  pntlemr  27911  pntlemf  27914  pntlemk  27915  pntlemo  27916  flt4lem5e  27968  flt4lem5f  27969  colinearalglem4  29469  axpasch  29501  axcontlem2  29525  axcontlem4  29527  axcontlem7  29530  axcontlem8  29531  ipasslem4  31418  minvecolem2  31459  his35  31672  leopnmid  32722  quad3d  33323  zringfrac  34068  ccfldsrarelvec  34285  constrrtll  34345  constrrtlc1  34346  constrrtcclem  34348  constrrtcc  34349  cos9thpiminplylem2  34397  oddpwdc  34969  prodfzo03  35215  itgexpif  35218  breprexplemc  35244  circlemeth  35252  hgt750lemg  35266  hgt750lemb  35268  hgt750leme  35270  subfacval2  35921  subfaclim  35922  circum  36408  faclimlem1  36477  faclimlem3  36479  faclim2  36482  unbdqndv2lem1  37345  knoppndvlem2  37349  knoppndvlem7  37354  knoppndvlem11  37358  knoppndvlem12  37359  knoppndvlem14  37361  knoppndvlem18  37365  itgmulc2nc  38574  areacirclem1  38594  areacirclem4  38597  bfplem1  38724  lcmineqlem1  43047  lcmineqlem5  43051  lcmineqlem10  43056  lcmineqlem12  43058  lcmineqlem18  43064  lcmineqlem20  43066  dvrelogpow2b  43086  aks4d1p1p7  43092  primrootscoprmpow  43117  2np3bcnp1  43162  quadfac  43223  remulcan2d  43275  remul02  43424  remul01  43426  sn-it0e0  43435  remulinvcom  43452  remullid  43453  sn-mullid  43455  remulcand  43458  rediveud  43462  redivrec2d  43479  rediv23d  43480  sn-0tie0  43483  sn-mul02  43484  mulgt0b1d  43504  mulgt0b2d  43510  mullt0b1d  43515  sn-itrere  43520  sn-retire  43521  fltnlta  43628  cu3addd  43645  3cubeslem2  43649  3cubeslem3l  43650  3cubeslem3r  43651  pellexlem6  43794  rmxluc  43896  rmyluc2  43898  rmydbl  43900  jm2.18  43948  jm2.23  43956  jm2.27c  43967  jm3.1lem2  43978  proot1ex  44156  sqrtcval  44600  sqrtcval2  44601  int-mulassocd  45136  binomcxplemnotnn0  45299  mul13d  46239  fmul01lt1lem1  46540  fmul01lt1lem2  46541  coskpi2  46820  cosknegpi  46823  dvnxpaek  46896  dvmptfprodlem  46898  dvnprodlem2  46901  itgsinexplem1  46908  stoweidlem26  46980  wallispilem5  47023  wallispi  47024  wallispi2lem1  47025  wallispi2lem2  47026  stirlinglem3  47030  stirlinglem10  47037  stirlinglem15  47042  dirkertrigeqlem1  47052  dirkertrigeqlem2  47053  dirkertrigeqlem3  47054  dirkertrigeq  47055  dirkercncflem2  47058  fourierdlem66  47126  fourierswlem  47184  fouriersw  47185  etransclem23  47211  etransclem25  47213  etransclem46  47234  hoidmvlelem2  47550  sigarls  47811  sharhght  47819  sin3t  47861  cos3t  47862  sin5tlem2  47864  sin5tlem3  47865  sin5tlem4  47866  modmkpkne  48381  fmtnorec4  48578  fmtnoprmfac2lem1  48595  fmtnoprmfac2  48596  fmtnofac2lem  48597  fmtnofac1  48599  lighneallem4a  48637  perfectALTVlem1  48763  perfectALTVlem2  48764  perfectALTV  48765  2zrngmmgm  49293  altgsumbcALT  49409  nn0sumshdiglemB  49676  affinecomb2  49759  itscnhlc0yqe  49815  itschlc0yqe  49816  itsclc0yqsollem1  49818  itsclc0yqsol  49820  itscnhlc0xyqsol  49821  itsclc0xyqsolr  49825  itsclquadb  49832  aacllem  50883  crosspdotd  50909  crossp3d  50911