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

Theorem mulassd 9112
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 9079 . 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 6082   CCcc 8989    x. cmul 8996
This theorem is referenced by:  recex  9655  mulcand  9656  receu  9668  divdivdiv  9716  divmuleq  9720  conjmul  9732  modmul1  11280  moddi  11285  expadd  11423  binom3  11501  digit1  11514  discr1  11516  discr  11517  faclbnd  11582  faclbnd6  11591  bcm1k  11607  bcp1nk  11609  crre  11920  remullem  11934  amgm2  12174  iseraltlem2  12477  iseraltlem3  12478  binomlem  12609  climcndslem2  12631  geo2sum  12651  mertenslem1  12662  sinadd  12766  tanadd  12769  bezoutlem3  13041  dvdsmulgcd  13055  qredeq  13107  pcaddlem  13258  prmpwdvds  13273  ablfacrp  15625  nmoco  18772  cph2ass  19176  minveclem2  19328  uniioombllem5  19480  itg1mulc  19597  mbfi1fseqlem5  19612  itgconst  19711  itgmulc2  19726  dvexp  19840  dvply1  20202  elqaalem3  20239  aalioulem1  20250  aaliou3lem2  20261  dvtaylp  20287  dvradcnv  20338  pserdvlem2  20345  tangtx  20414  tanregt0  20442  tanarg  20515  logcnlem4  20537  cxpmul  20580  dvcxp1  20627  root1eq1  20640  quad2  20680  dcubic1lem  20684  dcubic1  20686  cubic2  20689  binom4  20691  dquartlem1  20692  dquartlem2  20693  dquart  20694  quart1lem  20696  quart1  20697  quartlem1  20698  efiasin  20729  asinsinlem  20732  asinsin  20733  efiatan  20753  efiatan2  20758  2efiatan  20759  atantan  20764  atanbndlem  20766  atans2  20772  atantayl  20778  log2cnv  20785  log2tlbnd  20786  ftalem1  20856  ftalem5  20860  basellem3  20866  basellem5  20868  basellem8  20871  chtub  20997  perfectlem1  21014  perfectlem2  21015  perfect  21016  bcmono  21062  bclbnd  21065  bposlem9  21077  lgsneg  21104  lgseisenlem1  21134  lgseisenlem2  21135  lgseisenlem3  21136  lgseisenlem4  21137  lgsquad2lem1  21143  lgsquad3  21146  2sqlem3  21151  chto1ub  21171  rplogsumlem1  21179  dchrmusum2  21189  dchrvmasum2lem  21191  dchrvmasumlem2  21193  dchrvmasumiflem2  21197  dchrisum0lem1  21211  dchrisum0lem2  21213  mulog2sumlem2  21230  chpdifbndlem1  21248  selberg3lem1  21252  selberg4lem1  21255  selberg34r  21266  pntrlog2bndlem3  21274  pntrlog2bndlem5  21276  pntrlog2bndlem6  21278  pntlemh  21294  pntlemr  21297  pntlemf  21300  pntlemk  21301  pntlemo  21302  ipasslem4  22336  minvecolem2  22378  his35  22591  leopnmid  23642  subfacval2  24874  subfaclim  24875  circum  25112  clim2prod  25217  fallrisefac  25342  binomfallfaclem2  25357  faclimlem1  25363  faclimlem3  25365  faclim2  25368  colinearalglem4  25849  axpasch  25881  axcontlem2  25905  axcontlem4  25907  axcontlem7  25910  axcontlem8  25911  bpolydiflem  26101  bpoly4  26106  itgmulc2nc  26274  dvreasin  26291  areacirclem1  26293  areacirclem4  26296  csbrn  26457  bfplem1  26532  pellexlem6  26898  rmxluc  27000  rmyluc2  27002  rmydbl  27004  jm2.18  27060  jm2.23  27068  jm2.27c  27079  jm3.1lem2  27090  proot1ex  27498  fmul01lt1lem1  27691  fmul01lt1lem2  27692  itgsinexplem1  27725  stoweidlem26  27752  wallispilem5  27795  wallispi  27796  wallispi2lem1  27797  wallispi2lem2  27798  stirlinglem3  27802  stirlinglem10  27809  stirlinglem15  27814  sigarls  27824  sharhght  27832
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulass 9057
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator