Theorem mulassd 11007

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878   · cmul 10885

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088

This theorem is referenced by:  recex  11616  mulcand  11617  receu  11629  divmulasscom  11666  divdivdiv  11685  divmuleq  11689  conjmul  11701  modmul1  13653  moddi  13668  expadd  13834  mulbinom2  13947  binom3  13948  digit1  13961  discr1  13963  discr  13964  faclbnd  14013  faclbnd6  14022  bcm1k  14038  bcp1nk  14040  crre  14834  remullem  14848  amgm2  15090  iseraltlem2  15403  iseraltlem3  15404  binomlem  15550  climcndslem2  15571  pwdif  15589  geo2sum  15594  mertenslem1  15605  clim2prod  15609  fallrisefac  15744  binomfallfaclem2  15759  bpolydiflem  15773  bpoly4  15778  sinadd  15882  tanadd  15885  pwp1fsum  16109  bezoutlem3  16258  dvdsmulgcd  16274  qredeq  16371  pcaddlem  16598  prmpwdvds  16614  ablfacrp  19678  nmoco  23910  cph2ass  24386  cphipval2  24414  csbren  24572  minveclem2  24599  uniioombllem5  24760  itg1mulc  24878  mbfi1fseqlem5  24893  itgconst  24992  itgmulc2  25007  dvexp  25126  dvply1  25453  elqaalem3  25490  aalioulem1  25501  aaliou3lem2  25512  dvtaylp  25538  dvradcnv  25589  pserdvlem2  25596  tangtx  25671  tanregt0  25704  tanarg  25783  logcnlem4  25809  cxpmul  25852  dvcxp1  25902  dvcncxp1  25905  root1eq1  25917  heron  25997  quad2  25998  dcubic1lem  26002  dcubic1  26004  cubic2  26007  binom4  26009  dquartlem1  26010  dquartlem2  26011  dquart  26012  quart1lem  26014  quart1  26015  quartlem1  26016  efiasin  26047  asinsinlem  26050  asinsin  26051  efiatan  26071  efiatan2  26076  2efiatan  26077  atantan  26082  atanbndlem  26084  atans2  26090  atantayl  26096  log2cnv  26103  log2tlbnd  26104  ftalem1  26231  ftalem5  26235  basellem3  26241  basellem5  26243  basellem8  26246  chtub  26369  perfectlem1  26386  perfectlem2  26387  perfect  26388  bcmono  26434  bclbnd  26437  bposlem9  26449  lgsneg  26478  gausslemma2dlem6  26529  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem3  26534  lgseisenlem4  26535  lgsquad2lem1  26541  lgsquad3  26544  2lgslem3a  26553  2lgslem3b  26554  2lgslem3c  26555  2lgslem3d  26556  2lgsoddprmlem2  26566  2sqlem3  26577  chto1ub  26633  rplogsumlem1  26641  dchrmusum2  26651  dchrvmasum2lem  26653  dchrvmasumlem2  26655  dchrvmasumiflem2  26659  dchrisum0lem1  26673  dchrisum0lem2  26675  mulog2sumlem2  26692  chpdifbndlem1  26710  selberg3lem1  26714  selberg4lem1  26717  selberg34r  26728  pntrlog2bndlem3  26736  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntlemh  26756  pntlemr  26759  pntlemf  26762  pntlemk  26763  pntlemo  26764  colinearalglem4  27286  axpasch  27318  axcontlem2  27342  axcontlem4  27344  axcontlem7  27347  axcontlem8  27348  ipasslem4  29205  minvecolem2  29246  his35  29459  leopnmid  30509  ccfldsrarelvec  31750  oddpwdc  32330  prodfzo03  32592  itgexpif  32595  breprexplemc  32621  circlemeth  32629  hgt750lemg  32643  hgt750lemb  32645  hgt750leme  32647  subfacval2  33158  subfaclim  33159  circum  33641  faclimlem1  33718  faclimlem3  33720  faclim2  33723  unbdqndv2lem1  34698  knoppndvlem2  34702  knoppndvlem7  34707  knoppndvlem11  34711  knoppndvlem12  34712  knoppndvlem14  34714  knoppndvlem18  34718  itgmulc2nc  35854  areacirclem1  35874  areacirclem4  35877  bfplem1  35989  lcmineqlem1  40044  lcmineqlem5  40048  lcmineqlem10  40053  lcmineqlem12  40055  lcmineqlem18  40061  lcmineqlem20  40063  dvrelogpow2b  40083  aks4d1p1p7  40089  2np3bcnp1  40107  remulcan2d  40300  remul02  40395  remul01  40397  sn-it0e0  40404  remulinvcom  40421  remulid2  40422  sn-mulid2  40424  remulcand  40427  sn-0tie0  40428  sn-mul02  40429  mulgt0b2d  40437  itrere  40443  retire  40444  flt4lem5e  40500  flt4lem5f  40501  fltnlta  40507  cu3addd  40509  3cubeslem2  40514  3cubeslem3l  40515  3cubeslem3r  40516  pellexlem6  40663  rmxluc  40765  rmyluc2  40767  rmydbl  40769  jm2.18  40817  jm2.23  40825  jm2.27c  40836  jm3.1lem2  40847  proot1ex  41033  sqrtcval  41256  sqrtcval2  41257  int-mulassocd  41795  binomcxplemnotnn0  41981  mul13d  42825  fmul01lt1lem1  43132  fmul01lt1lem2  43133  coskpi2  43414  cosknegpi  43417  dvnxpaek  43490  dvmptfprodlem  43492  dvnprodlem2  43495  itgsinexplem1  43502  stoweidlem26  43574  wallispilem5  43617  wallispi  43618  wallispi2lem1  43619  wallispi2lem2  43620  stirlinglem3  43624  stirlinglem10  43631  stirlinglem15  43636  dirkertrigeqlem1  43646  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkercncflem2  43652  fourierdlem66  43720  fourierswlem  43778  fouriersw  43779  etransclem23  43805  etransclem25  43807  etransclem46  43828  hoidmvlelem2  44141  sigarls  44384  sharhght  44392  fmtnorec4  45012  fmtnoprmfac2lem1  45029  fmtnoprmfac2  45030  fmtnofac2lem  45031  fmtnofac1  45033  lighneallem4a  45071  perfectALTVlem1  45184  perfectALTVlem2  45185  perfectALTV  45186  2zrngmmgm  45515  altgsumbcALT  45700  nn0sumshdiglemB  45977  affinecomb2  46060  itscnhlc0yqe  46116  itschlc0yqe  46117  itsclc0yqsollem1  46119  itsclc0yqsol  46121  itscnhlc0xyqsol  46122  itsclc0xyqsolr  46126  itsclquadb  46133  aacllem  46516