Theorem mulassd 11260

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 11216	. 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 7417  ℂcc 11126   · cmul 11133

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

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

This theorem is used by:  recex  11874  mulcand  11875  receu  11887  divmulasscom  11924  divdivdiv  11944  divmuleq  11948  conjmul  11960  modmul1  13992  moddi  14007  expadd  14172  mulbinom2  14291  binom3  14292  digit1  14305  discr1  14307  discr  14308  faclbnd  14358  faclbnd6  14367  bcm1k  14383  bcp1nk  14385  crre  15205  remullem  15219  amgm2  15461  iseraltlem2  15774  iseraltlem3  15775  binomlem  15922  climcndslem2  15943  pwdif  15961  geo2sum  15966  mertenslem1  15977  clim2prod  15981  fallrisefac  16118  binomfallfaclem2  16132  bpolydiflem  16146  bpoly4  16151  sinadd  16258  tanadd  16261  pwp1fsum  16487  bezoutlem3  16637  dvdsmulgcd  16652  qredeq  16753  pcaddlem  16986  prmpwdvds  17002  ablfacrp  20201  nmoco  24969  cph2ass  25447  cphipval2  25475  csbren  25633  minveclem2  25660  uniioombllem5  25821  itg1mulc  25938  mbfi1fseqlem5  25953  itgconst  26053  itgmulc2  26068  dvexp  26187  dvply1  26521  elqaalem3  26560  aalioulem1  26575  aaliou3lem2  26586  dvtaylp  26613  dvradcnv  26664  pserdvlem2  26671  tangtx  26750  tanregt0  26784  tanarg  26864  logcnlem4  26890  cxpmul  26933  dvcxp1  26985  dvcncxp1  26988  root1eq1  27000  heron  27083  quad2  27084  dcubic1lem  27088  dcubic1  27090  cubic2  27093  binom4  27095  dquartlem1  27096  dquartlem2  27097  dquart  27098  quart1lem  27100  quart1  27101  quartlem1  27102  efiasin  27133  asinsinlem  27136  asinsin  27137  efiatan  27157  efiatan2  27162  2efiatan  27163  atantan  27168  atanbndlem  27170  atans2  27176  atantayl  27182  log2cnv  27189  log2tlbnd  27190  ftalem1  27317  ftalem5  27321  basellem3  27327  basellem5  27329  basellem8  27332  chtub  27456  perfectlem1  27473  perfectlem2  27474  perfect  27475  bcmono  27521  bclbnd  27524  bposlem9  27536  lgsneg  27565  gausslemma2dlem6  27616  lgseisenlem1  27619  lgseisenlem2  27620  lgseisenlem3  27621  lgseisenlem4  27622  lgsquad2lem1  27628  lgsquad3  27631  2lgslem3a  27640  2lgslem3b  27641  2lgslem3c  27642  2lgslem3d  27643  2lgsoddprmlem2  27653  2sqlem3  27664  chto1ub  27720  rplogsumlem1  27728  dchrmusum2  27738  dchrvmasum2lem  27740  dchrvmasumlem2  27742  dchrvmasumiflem2  27746  dchrisum0lem1  27760  dchrisum0lem2  27762  mulog2sumlem2  27779  chpdifbndlem1  27797  selberg3lem1  27801  selberg4lem1  27804  selberg34r  27815  pntrlog2bndlem3  27823  pntrlog2bndlem5  27825  pntrlog2bndlem6  27827  pntlemh  27843  pntlemr  27846  pntlemf  27849  pntlemk  27850  pntlemo  27851  colinearalglem4  29374  axpasch  29406  axcontlem2  29430  axcontlem4  29432  axcontlem7  29435  axcontlem8  29436  ipasslem4  31323  minvecolem2  31364  his35  31577  leopnmid  32627  quad3d  33228  zringfrac  33972  ccfldsrarelvec  34189  constrrtll  34249  constrrtlc1  34250  constrrtcclem  34252  constrrtcc  34253  cos9thpiminplylem2  34301  oddpwdc  34873  prodfzo03  35119  itgexpif  35122  breprexplemc  35148  circlemeth  35156  hgt750lemg  35170  hgt750lemb  35172  hgt750leme  35174  subfacval2  35774  subfaclim  35775  circum  36261  faclimlem1  36330  faclimlem3  36332  faclim2  36335  unbdqndv2lem1  37214  knoppndvlem2  37218  knoppndvlem7  37223  knoppndvlem11  37227  knoppndvlem12  37228  knoppndvlem14  37230  knoppndvlem18  37234  itgmulc2nc  38445  areacirclem1  38465  areacirclem4  38468  bfplem1  38580  lcmineqlem1  42903  lcmineqlem5  42907  lcmineqlem10  42912  lcmineqlem12  42914  lcmineqlem18  42920  lcmineqlem20  42922  dvrelogpow2b  42942  aks4d1p1p7  42948  primrootscoprmpow  42973  2np3bcnp1  43018  quadfac  43079  remulcan2d  43131  remul02  43288  remul01  43290  sn-it0e0  43299  remulinvcom  43316  remullid  43317  sn-mullid  43319  remulcand  43322  rediveud  43326  redivrec2d  43343  rediv23d  43344  sn-0tie0  43347  sn-mul02  43348  mulgt0b1d  43368  mulgt0b2d  43374  mullt0b1d  43379  sn-itrere  43384  sn-retire  43385  flt4lem5e  43510  flt4lem5f  43511  fltnlta  43517  cu3addd  43534  3cubeslem2  43538  3cubeslem3l  43539  3cubeslem3r  43540  pellexlem6  43683  rmxluc  43785  rmyluc2  43787  rmydbl  43789  jm2.18  43837  jm2.23  43845  jm2.27c  43856  jm3.1lem2  43867  proot1ex  44045  sqrtcval  44489  sqrtcval2  44490  int-mulassocd  45025  binomcxplemnotnn0  45188  mul13d  46121  fmul01lt1lem1  46422  fmul01lt1lem2  46423  coskpi2  46702  cosknegpi  46705  dvnxpaek  46778  dvmptfprodlem  46780  dvnprodlem2  46783  itgsinexplem1  46790  stoweidlem26  46862  wallispilem5  46905  wallispi  46906  wallispi2lem1  46907  wallispi2lem2  46908  stirlinglem3  46912  stirlinglem10  46919  stirlinglem15  46924  dirkertrigeqlem1  46934  dirkertrigeqlem2  46935  dirkertrigeqlem3  46936  dirkertrigeq  46937  dirkercncflem2  46940  fourierdlem66  47008  fourierswlem  47066  fouriersw  47067  etransclem23  47093  etransclem25  47095  etransclem46  47116  hoidmvlelem2  47432  sigarls  47693  sharhght  47701  sin3t  47743  cos3t  47744  sin5tlem2  47746  sin5tlem3  47747  sin5tlem4  47748  modmkpkne  48263  fmtnorec4  48460  fmtnoprmfac2lem1  48477  fmtnoprmfac2  48478  fmtnofac2lem  48479  fmtnofac1  48481  lighneallem4a  48519  perfectALTVlem1  48645  perfectALTVlem2  48646  perfectALTV  48647  2zrngmmgm  49175  altgsumbcALT  49291  nn0sumshdiglemB  49558  affinecomb2  49641  itscnhlc0yqe  49697  itschlc0yqe  49698  itsclc0yqsollem1  49700  itsclc0yqsol  49702  itscnhlc0xyqsol  49703  itsclc0xyqsolr  49707  itsclquadb  49714  aacllem  50780  crosspdotd  50806  crossp3d  50808