MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulassd Structured version   Unicode version

Theorem mulassd 9116
Description: Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
addassd.3  |-  ( ph  ->  C  e.  CC )
Assertion
Ref Expression
mulassd  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( A  x.  ( B  x.  C ) ) )

Proof of Theorem mulassd
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 addassd.3 . 2  |-  ( ph  ->  C  e.  CC )
4 mulass 9083 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1185 1  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( A  x.  ( B  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726  (class class class)co 6084   CCcc 8993    x. cmul 9000
This theorem is referenced by:  recex  9659  mulcand  9660  receu  9672  divdivdiv  9720  divmuleq  9724  conjmul  9736  modmul1  11284  moddi  11289  expadd  11427  binom3  11505  digit1  11518  discr1  11520  discr  11521  faclbnd  11586  faclbnd6  11595  bcm1k  11611  bcp1nk  11613  crre  11924  remullem  11938  amgm2  12178  iseraltlem2  12481  iseraltlem3  12482  binomlem  12613  climcndslem2  12635  geo2sum  12655  mertenslem1  12666  sinadd  12770  tanadd  12773  bezoutlem3  13045  dvdsmulgcd  13059  qredeq  13111  pcaddlem  13262  prmpwdvds  13277  ablfacrp  15629  nmoco  18776  cph2ass  19180  minveclem2  19332  uniioombllem5  19484  itg1mulc  19599  mbfi1fseqlem5  19614  itgconst  19713  itgmulc2  19728  dvexp  19844  dvply1  20206  elqaalem3  20243  aalioulem1  20254  aaliou3lem2  20265  dvtaylp  20291  dvradcnv  20342  pserdvlem2  20349  tangtx  20418  tanregt0  20446  tanarg  20519  logcnlem4  20541  cxpmul  20584  dvcxp1  20631  root1eq1  20644  quad2  20684  dcubic1lem  20688  dcubic1  20690  cubic2  20693  binom4  20695  dquartlem1  20696  dquartlem2  20697  dquart  20698  quart1lem  20700  quart1  20701  quartlem1  20702  efiasin  20733  asinsinlem  20736  asinsin  20737  efiatan  20757  efiatan2  20762  2efiatan  20763  atantan  20768  atanbndlem  20770  atans2  20776  atantayl  20782  log2cnv  20789  log2tlbnd  20790  ftalem1  20860  ftalem5  20864  basellem3  20870  basellem5  20872  basellem8  20875  chtub  21001  perfectlem1  21018  perfectlem2  21019  perfect  21020  bcmono  21066  bclbnd  21069  bposlem9  21081  lgsneg  21108  lgseisenlem1  21138  lgseisenlem2  21139  lgseisenlem3  21140  lgseisenlem4  21141  lgsquad2lem1  21147  lgsquad3  21150  2sqlem3  21155  chto1ub  21175  rplogsumlem1  21183  dchrmusum2  21193  dchrvmasum2lem  21195  dchrvmasumlem2  21197  dchrvmasumiflem2  21201  dchrisum0lem1  21215  dchrisum0lem2  21217  mulog2sumlem2  21234  chpdifbndlem1  21252  selberg3lem1  21256  selberg4lem1  21259  selberg34r  21270  pntrlog2bndlem3  21278  pntrlog2bndlem5  21280  pntrlog2bndlem6  21282  pntlemh  21298  pntlemr  21301  pntlemf  21304  pntlemk  21305  pntlemo  21306  ipasslem4  22340  minvecolem2  22382  his35  22595  leopnmid  23646  subfacval2  24878  subfaclim  24879  circum  25116  clim2prod  25221  fallrisefac  25346  binomfallfaclem2  25361  faclimlem1  25367  faclimlem3  25369  faclim2  25372  colinearalglem4  25853  axpasch  25885  axcontlem2  25909  axcontlem4  25911  axcontlem7  25914  axcontlem8  25915  bpolydiflem  26105  bpoly4  26110  itgmulc2nc  26287  dvreasin  26304  areacirclem1  26306  areacirclem4  26309  csbrn  26470  bfplem1  26545  pellexlem6  26911  rmxluc  27013  rmyluc2  27015  rmydbl  27017  jm2.18  27073  jm2.23  27081  jm2.27c  27092  jm3.1lem2  27103  proot1ex  27511  fmul01lt1lem1  27704  fmul01lt1lem2  27705  itgsinexplem1  27738  stoweidlem26  27765  wallispilem5  27808  wallispi  27809  wallispi2lem1  27810  wallispi2lem2  27811  stirlinglem3  27815  stirlinglem10  27822  stirlinglem15  27827  sigarls  27837  sharhght  27845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 9061
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator