Theorem mulassd 10653

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   · cmul 10531

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086

This theorem is referenced by:  recex  11261  mulcand  11262  receu  11274  divmulasscom  11311  divdivdiv  11330  divmuleq  11334  conjmul  11346  modmul1  13287  moddi  13302  expadd  13467  mulbinom2  13580  binom3  13581  digit1  13594  discr1  13596  discr  13597  faclbnd  13646  faclbnd6  13655  bcm1k  13671  bcp1nk  13673  crre  14465  remullem  14479  amgm2  14721  iseraltlem2  15031  iseraltlem3  15032  binomlem  15176  climcndslem2  15197  pwdif  15215  geo2sum  15221  mertenslem1  15232  clim2prod  15236  fallrisefac  15371  binomfallfaclem2  15386  bpolydiflem  15400  bpoly4  15405  sinadd  15509  tanadd  15512  pwp1fsum  15732  bezoutlem3  15879  dvdsmulgcd  15895  qredeq  15991  pcaddlem  16214  prmpwdvds  16230  ablfacrp  19181  nmoco  23343  cph2ass  23818  cphipval2  23845  csbren  24003  minveclem2  24030  uniioombllem5  24191  itg1mulc  24308  mbfi1fseqlem5  24323  itgconst  24422  itgmulc2  24437  dvexp  24556  dvply1  24880  elqaalem3  24917  aalioulem1  24928  aaliou3lem2  24939  dvtaylp  24965  dvradcnv  25016  pserdvlem2  25023  tangtx  25098  tanregt0  25131  tanarg  25210  logcnlem4  25236  cxpmul  25279  dvcxp1  25329  dvcncxp1  25332  root1eq1  25344  heron  25424  quad2  25425  dcubic1lem  25429  dcubic1  25431  cubic2  25434  binom4  25436  dquartlem1  25437  dquartlem2  25438  dquart  25439  quart1lem  25441  quart1  25442  quartlem1  25443  efiasin  25474  asinsinlem  25477  asinsin  25478  efiatan  25498  efiatan2  25503  2efiatan  25504  atantan  25509  atanbndlem  25511  atans2  25517  atantayl  25523  log2cnv  25530  log2tlbnd  25531  ftalem1  25658  ftalem5  25662  basellem3  25668  basellem5  25670  basellem8  25673  chtub  25796  perfectlem1  25813  perfectlem2  25814  perfect  25815  bcmono  25861  bclbnd  25864  bposlem9  25876  lgsneg  25905  gausslemma2dlem6  25956  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem3  25961  lgseisenlem4  25962  lgsquad2lem1  25968  lgsquad3  25971  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  2lgsoddprmlem2  25993  2sqlem3  26004  chto1ub  26060  rplogsumlem1  26068  dchrmusum2  26078  dchrvmasum2lem  26080  dchrvmasumlem2  26082  dchrvmasumiflem2  26086  dchrisum0lem1  26100  dchrisum0lem2  26102  mulog2sumlem2  26119  chpdifbndlem1  26137  selberg3lem1  26141  selberg4lem1  26144  selberg34r  26155  pntrlog2bndlem3  26163  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  pntlemh  26183  pntlemr  26186  pntlemf  26189  pntlemk  26190  pntlemo  26191  colinearalglem4  26703  axpasch  26735  axcontlem2  26759  axcontlem4  26761  axcontlem7  26764  axcontlem8  26765  ipasslem4  28617  minvecolem2  28658  his35  28871  leopnmid  29921  ccfldsrarelvec  31144  oddpwdc  31722  prodfzo03  31984  itgexpif  31987  breprexplemc  32013  circlemeth  32021  hgt750lemg  32035  hgt750lemb  32037  hgt750leme  32039  subfacval2  32547  subfaclim  32548  circum  33030  faclimlem1  33088  faclimlem3  33090  faclim2  33093  unbdqndv2lem1  33961  knoppndvlem2  33965  knoppndvlem7  33970  knoppndvlem11  33974  knoppndvlem12  33975  knoppndvlem14  33977  knoppndvlem18  33981  itgmulc2nc  35125  areacirclem1  35145  areacirclem4  35148  bfplem1  35260  lcmineqlem1  39317  lcmineqlem5  39321  lcmineqlem10  39326  lcmineqlem12  39328  lcmineqlem18  39334  lcmineqlem20  39336  3lexlogpow5ineq2  39342  2np3bcnp1  39348  remulcan2d  39464  remul02  39543  remul01  39545  sn-it0e0  39552  remulinvcom  39569  remulid2  39570  sn-mulid2  39572  remulcand  39575  sn-0tie0  39576  sn-mul02  39577  mulgt0b2d  39585  itrere  39591  retire  39592  fltnlta  39619  cu3addd  39621  3cubeslem2  39626  3cubeslem3l  39627  3cubeslem3r  39628  pellexlem6  39775  rmxluc  39877  rmyluc2  39879  rmydbl  39881  jm2.18  39929  jm2.23  39937  jm2.27c  39948  jm3.1lem2  39959  proot1ex  40145  sqrtcval  40341  sqrtcval2  40342  int-mulassocd  40883  binomcxplemnotnn0  41060  mul13d  41910  fmul01lt1lem1  42226  fmul01lt1lem2  42227  coskpi2  42508  cosknegpi  42511  dvnxpaek  42584  dvmptfprodlem  42586  dvnprodlem2  42589  itgsinexplem1  42596  stoweidlem26  42668  wallispilem5  42711  wallispi  42712  wallispi2lem1  42713  wallispi2lem2  42714  stirlinglem3  42718  stirlinglem10  42725  stirlinglem15  42730  dirkertrigeqlem1  42740  dirkertrigeqlem2  42741  dirkertrigeqlem3  42742  dirkertrigeq  42743  dirkercncflem2  42746  fourierdlem66  42814  fourierswlem  42872  fouriersw  42873  etransclem23  42899  etransclem25  42901  etransclem46  42922  hoidmvlelem2  43235  sigarls  43471  sharhght  43479  fmtnorec4  44066  fmtnoprmfac2lem1  44083  fmtnoprmfac2  44084  fmtnofac2lem  44085  fmtnofac1  44087  lighneallem4a  44126  perfectALTVlem1  44239  perfectALTVlem2  44240  perfectALTV  44241  2zrngmmgm  44570  altgsumbcALT  44755  nn0sumshdiglemB  45034  affinecomb2  45117  itscnhlc0yqe  45173  itschlc0yqe  45174  itsclc0yqsollem1  45176  itsclc0yqsol  45178  itscnhlc0xyqsol  45179  itsclc0xyqsolr  45183  itsclquadb  45190  aacllem  45329