Theorem mulassd 11168

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 7367  ℂ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  11782  mulcand  11783  receu  11795  divmulasscom  11833  divdivdiv  11856  divmuleq  11860  conjmul  11872  modmul1  13886  moddi  13901  expadd  14066  mulbinom2  14185  binom3  14186  digit1  14199  discr1  14201  discr  14202  faclbnd  14252  faclbnd6  14261  bcm1k  14277  bcp1nk  14279  crre  15076  remullem  15090  amgm2  15332  iseraltlem2  15645  iseraltlem3  15646  binomlem  15794  climcndslem2  15815  pwdif  15833  geo2sum  15838  mertenslem1  15849  clim2prod  15853  fallrisefac  15990  binomfallfaclem2  16005  bpolydiflem  16019  bpoly4  16024  sinadd  16131  tanadd  16134  pwp1fsum  16360  bezoutlem3  16510  dvdsmulgcd  16525  qredeq  16626  pcaddlem  16859  prmpwdvds  16875  ablfacrp  20043  nmoco  24702  cph2ass  25180  cphipval2  25208  csbren  25366  minveclem2  25393  uniioombllem5  25554  itg1mulc  25671  mbfi1fseqlem5  25686  itgconst  25786  itgmulc2  25801  dvexp  25920  dvply1  26250  elqaalem3  26287  aalioulem1  26298  aaliou3lem2  26309  dvtaylp  26335  dvradcnv  26386  pserdvlem2  26393  tangtx  26469  tanregt0  26503  tanarg  26583  logcnlem4  26609  cxpmul  26652  dvcxp1  26704  dvcncxp1  26707  root1eq1  26719  heron  26802  quad2  26803  dcubic1lem  26807  dcubic1  26809  cubic2  26812  binom4  26814  dquartlem1  26815  dquartlem2  26816  dquart  26817  quart1lem  26819  quart1  26820  quartlem1  26821  efiasin  26852  asinsinlem  26855  asinsin  26856  efiatan  26876  efiatan2  26881  2efiatan  26882  atantan  26887  atanbndlem  26889  atans2  26895  atantayl  26901  log2cnv  26908  log2tlbnd  26909  ftalem1  27036  ftalem5  27040  basellem3  27046  basellem5  27048  basellem8  27051  chtub  27175  perfectlem1  27192  perfectlem2  27193  perfect  27194  bcmono  27240  bclbnd  27243  bposlem9  27255  lgsneg  27284  gausslemma2dlem6  27335  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgsquad2lem1  27347  lgsquad3  27350  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2lgsoddprmlem2  27372  2sqlem3  27383  chto1ub  27439  rplogsumlem1  27447  dchrmusum2  27457  dchrvmasum2lem  27459  dchrvmasumlem2  27461  dchrvmasumiflem2  27465  dchrisum0lem1  27479  dchrisum0lem2  27481  mulog2sumlem2  27498  chpdifbndlem1  27516  selberg3lem1  27520  selberg4lem1  27523  selberg34r  27534  pntrlog2bndlem3  27542  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntlemh  27562  pntlemr  27565  pntlemf  27568  pntlemk  27569  pntlemo  27570  colinearalglem4  28978  axpasch  29010  axcontlem2  29034  axcontlem4  29036  axcontlem7  29039  axcontlem8  29040  ipasslem4  30905  minvecolem2  30946  his35  31159  leopnmid  32209  quad3d  32822  zringfrac  33614  ccfldsrarelvec  33815  constrrtll  33875  constrrtlc1  33876  constrrtcclem  33878  constrrtcc  33879  cos9thpiminplylem2  33927  oddpwdc  34498  prodfzo03  34747  itgexpif  34750  breprexplemc  34776  circlemeth  34784  hgt750lemg  34798  hgt750lemb  34800  hgt750leme  34802  subfacval2  35369  subfaclim  35370  circum  35856  faclimlem1  35925  faclimlem3  35927  faclim2  35930  unbdqndv2lem1  36769  knoppndvlem2  36773  knoppndvlem7  36778  knoppndvlem11  36782  knoppndvlem12  36783  knoppndvlem14  36785  knoppndvlem18  36789  itgmulc2nc  38009  areacirclem1  38029  areacirclem4  38032  bfplem1  38143  lcmineqlem1  42468  lcmineqlem5  42472  lcmineqlem10  42477  lcmineqlem12  42479  lcmineqlem18  42485  lcmineqlem20  42487  dvrelogpow2b  42507  aks4d1p1p7  42513  primrootscoprmpow  42538  2np3bcnp1  42583  remulcan2d  42695  remul02  42837  remul01  42839  sn-it0e0  42848  remulinvcom  42865  remullid  42866  sn-mullid  42868  remulcand  42871  rediveud  42875  redivrec2d  42892  rediv23d  42893  sn-0tie0  42896  sn-mul02  42897  mulgt0b1d  42917  mulgt0b2d  42923  mullt0b1d  42928  sn-itrere  42933  sn-retire  42934  flt4lem5e  43089  flt4lem5f  43090  fltnlta  43096  cu3addd  43113  3cubeslem2  43117  3cubeslem3l  43118  3cubeslem3r  43119  pellexlem6  43262  rmxluc  43364  rmyluc2  43366  rmydbl  43368  jm2.18  43416  jm2.23  43424  jm2.27c  43435  jm3.1lem2  43446  proot1ex  43624  sqrtcval  44068  sqrtcval2  44069  int-mulassocd  44604  binomcxplemnotnn0  44783  mul13d  45713  fmul01lt1lem1  46014  fmul01lt1lem2  46015  coskpi2  46294  cosknegpi  46297  dvnxpaek  46370  dvmptfprodlem  46372  dvnprodlem2  46375  itgsinexplem1  46382  stoweidlem26  46454  wallispilem5  46497  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  stirlinglem3  46504  stirlinglem10  46511  stirlinglem15  46516  dirkertrigeqlem1  46526  dirkertrigeqlem2  46527  dirkertrigeqlem3  46528  dirkertrigeq  46529  dirkercncflem2  46532  fourierdlem66  46600  fourierswlem  46658  fouriersw  46659  etransclem23  46685  etransclem25  46687  etransclem46  46708  hoidmvlelem2  47024  sigarls  47285  sharhght  47293  sin3t  47319  cos3t  47320  sin5tlem2  47322  sin5tlem3  47323  sin5tlem4  47324  modmkpkne  47815  fmtnorec4  48012  fmtnoprmfac2lem1  48029  fmtnoprmfac2  48030  fmtnofac2lem  48031  fmtnofac1  48033  lighneallem4a  48071  perfectALTVlem1  48197  perfectALTVlem2  48198  perfectALTV  48199  2zrngmmgm  48728  altgsumbcALT  48829  nn0sumshdiglemB  49096  affinecomb2  49179  itscnhlc0yqe  49235  itschlc0yqe  49236  itsclc0yqsollem1  49238  itsclc0yqsol  49240  itscnhlc0xyqsol  49241  itsclc0xyqsolr  49245  itsclquadb  49252  aacllem  50276