Theorem mulassd 11233

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   · cmul 11106

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is referenced by:  recex  11847  mulcand  11848  receu  11860  divmulasscom  11897  divdivdiv  11917  divmuleq  11921  conjmul  11933  modmul1  13962  moddi  13977  expadd  14142  mulbinom2  14261  binom3  14262  digit1  14275  discr1  14277  discr  14278  faclbnd  14328  faclbnd6  14337  bcm1k  14353  bcp1nk  14355  crre  15167  remullem  15181  amgm2  15423  iseraltlem2  15736  iseraltlem3  15737  binomlem  15885  climcndslem2  15906  pwdif  15924  geo2sum  15929  mertenslem1  15940  clim2prod  15944  fallrisefac  16081  binomfallfaclem2  16095  bpolydiflem  16109  bpoly4  16114  sinadd  16221  tanadd  16224  pwp1fsum  16450  bezoutlem3  16600  dvdsmulgcd  16615  qredeq  16716  pcaddlem  16949  prmpwdvds  16965  ablfacrp  20139  nmoco  24875  cph2ass  25353  cphipval2  25381  csbren  25539  minveclem2  25566  uniioombllem5  25727  itg1mulc  25844  mbfi1fseqlem5  25859  itgconst  25959  itgmulc2  25974  dvexp  26093  dvply1  26426  elqaalem3  26463  aalioulem1  26476  aaliou3lem2  26487  dvtaylp  26514  dvradcnv  26565  pserdvlem2  26572  tangtx  26651  tanregt0  26685  tanarg  26765  logcnlem4  26791  cxpmul  26834  dvcxp1  26886  dvcncxp1  26889  root1eq1  26901  heron  26984  quad2  26985  dcubic1lem  26989  dcubic1  26991  cubic2  26994  binom4  26996  dquartlem1  26997  dquartlem2  26998  dquart  26999  quart1lem  27001  quart1  27002  quartlem1  27003  efiasin  27034  asinsinlem  27037  asinsin  27038  efiatan  27058  efiatan2  27063  2efiatan  27064  atantan  27069  atanbndlem  27071  atans2  27077  atantayl  27083  log2cnv  27090  log2tlbnd  27091  ftalem1  27218  ftalem5  27222  basellem3  27228  basellem5  27230  basellem8  27233  chtub  27357  perfectlem1  27374  perfectlem2  27375  perfect  27376  bcmono  27422  bclbnd  27425  bposlem9  27437  lgsneg  27466  gausslemma2dlem6  27517  lgseisenlem1  27520  lgseisenlem2  27521  lgseisenlem3  27522  lgseisenlem4  27523  lgsquad2lem1  27529  lgsquad3  27532  2lgslem3a  27541  2lgslem3b  27542  2lgslem3c  27543  2lgslem3d  27544  2lgsoddprmlem2  27554  2sqlem3  27565  chto1ub  27621  rplogsumlem1  27629  dchrmusum2  27639  dchrvmasum2lem  27641  dchrvmasumlem2  27643  dchrvmasumiflem2  27647  dchrisum0lem1  27661  dchrisum0lem2  27663  mulog2sumlem2  27680  chpdifbndlem1  27698  selberg3lem1  27702  selberg4lem1  27705  selberg34r  27716  pntrlog2bndlem3  27724  pntrlog2bndlem5  27726  pntrlog2bndlem6  27728  pntlemh  27744  pntlemr  27747  pntlemf  27750  pntlemk  27751  pntlemo  27752  colinearalglem4  29240  axpasch  29272  axcontlem2  29296  axcontlem4  29298  axcontlem7  29301  axcontlem8  29302  ipasslem4  31167  minvecolem2  31208  his35  31421  leopnmid  32471  quad3d  33075  zringfrac  33825  ccfldsrarelvec  34042  constrrtll  34102  constrrtlc1  34103  constrrtcclem  34105  constrrtcc  34106  cos9thpiminplylem2  34154  oddpwdc  34725  prodfzo03  34971  itgexpif  34974  breprexplemc  35000  circlemeth  35008  hgt750lemg  35022  hgt750lemb  35024  hgt750leme  35026  subfacval2  35660  subfaclim  35661  circum  36147  faclimlem1  36216  faclimlem3  36218  faclim2  36221  unbdqndv2lem1  37079  knoppndvlem2  37083  knoppndvlem7  37088  knoppndvlem11  37092  knoppndvlem12  37093  knoppndvlem14  37095  knoppndvlem18  37099  itgmulc2nc  38320  areacirclem1  38340  areacirclem4  38343  bfplem1  38454  lcmineqlem1  42777  lcmineqlem5  42781  lcmineqlem10  42786  lcmineqlem12  42788  lcmineqlem18  42794  lcmineqlem20  42796  dvrelogpow2b  42816  aks4d1p1p7  42822  primrootscoprmpow  42847  2np3bcnp1  42892  quadfac  42953  remulcan2d  43005  remul02  43147  remul01  43149  sn-it0e0  43158  remulinvcom  43175  remullid  43176  sn-mullid  43178  remulcand  43181  rediveud  43185  redivrec2d  43202  rediv23d  43203  sn-0tie0  43206  sn-mul02  43207  mulgt0b1d  43227  mulgt0b2d  43233  mullt0b1d  43238  sn-itrere  43243  sn-retire  43244  flt4lem5e  43371  flt4lem5f  43372  fltnlta  43378  cu3addd  43395  3cubeslem2  43399  3cubeslem3l  43400  3cubeslem3r  43401  pellexlem6  43544  rmxluc  43646  rmyluc2  43648  rmydbl  43650  jm2.18  43698  jm2.23  43706  jm2.27c  43717  jm3.1lem2  43728  proot1ex  43906  sqrtcval  44350  sqrtcval2  44351  int-mulassocd  44886  binomcxplemnotnn0  45049  mul13d  45982  fmul01lt1lem1  46283  fmul01lt1lem2  46284  coskpi2  46563  cosknegpi  46566  dvnxpaek  46639  dvmptfprodlem  46641  dvnprodlem2  46644  itgsinexplem1  46651  stoweidlem26  46723  wallispilem5  46766  wallispi  46767  wallispi2lem1  46768  wallispi2lem2  46769  stirlinglem3  46773  stirlinglem10  46780  stirlinglem15  46785  dirkertrigeqlem1  46795  dirkertrigeqlem2  46796  dirkertrigeqlem3  46797  dirkertrigeq  46798  dirkercncflem2  46801  fourierdlem66  46869  fourierswlem  46927  fouriersw  46928  etransclem23  46954  etransclem25  46956  etransclem46  46977  hoidmvlelem2  47293  sigarls  47554  sharhght  47562  sin3t  47591  cos3t  47592  sin5tlem2  47594  sin5tlem3  47595  sin5tlem4  47596  modmkpkne  48087  fmtnorec4  48284  fmtnoprmfac2lem1  48301  fmtnoprmfac2  48302  fmtnofac2lem  48303  fmtnofac1  48305  lighneallem4a  48343  perfectALTVlem1  48469  perfectALTVlem2  48470  perfectALTV  48471  2zrngmmgm  49000  altgsumbcALT  49116  nn0sumshdiglemB  49383  affinecomb2  49466  itscnhlc0yqe  49522  itschlc0yqe  49523  itsclc0yqsollem1  49525  itsclc0yqsol  49527  itscnhlc0xyqsol  49528  itsclc0xyqsolr  49532  itsclquadb  49539  aacllem  50584