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

Theorem mulassd 8874
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 8841 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1182 1  |-  ( ph  ->  ( ( A  x.  B )  x.  C
)  =  ( A  x.  ( B  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    x. cmul 8758
This theorem is referenced by:  recex  9416  mulcand  9417  receu  9429  divdivdiv  9477  divmuleq  9481  conjmul  9493  modmul1  11018  moddi  11023  expadd  11160  binom3  11238  digit1  11251  discr1  11253  discr  11254  faclbnd  11319  faclbnd6  11328  bcm1k  11343  bcp1nk  11345  crre  11615  remullem  11629  amgm2  11869  iseraltlem2  12171  iseraltlem3  12172  binomlem  12303  climcndslem2  12325  geo2sum  12345  mertenslem1  12356  sinadd  12460  tanadd  12463  bezoutlem3  12735  dvdsmulgcd  12749  qredeq  12801  pcaddlem  12952  prmpwdvds  12967  ablfacrp  15317  nmoco  18262  cph2ass  18664  minveclem2  18806  uniioombllem5  18958  itg1mulc  19075  mbfi1fseqlem5  19090  itgconst  19189  itgmulc2  19204  dvexp  19318  dvply1  19680  elqaalem3  19717  aalioulem1  19728  aaliou3lem2  19739  dvtaylp  19765  dvradcnv  19813  pserdvlem2  19820  tangtx  19889  tanregt0  19917  tanarg  19986  logcnlem4  20008  cxpmul  20051  dvcxp1  20098  root1eq1  20111  quad2  20151  dcubic1lem  20155  dcubic1  20157  cubic2  20160  binom4  20162  dquartlem1  20163  dquartlem2  20164  dquart  20165  quart1lem  20167  quart1  20168  quartlem1  20169  efiasin  20200  asinsinlem  20203  asinsin  20204  efiatan  20224  efiatan2  20229  2efiatan  20230  atantan  20235  atanbndlem  20237  atans2  20243  atantayl  20249  log2cnv  20256  log2tlbnd  20257  ftalem1  20326  ftalem5  20330  basellem3  20336  basellem5  20338  basellem8  20341  chtub  20467  perfectlem1  20484  perfectlem2  20485  perfect  20486  bcmono  20532  bclbnd  20535  bposlem9  20547  lgsneg  20574  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem3  20606  lgseisenlem4  20607  lgsquad2lem1  20613  lgsquad3  20616  2sqlem3  20621  chto1ub  20641  rplogsumlem1  20649  dchrmusum2  20659  dchrvmasum2lem  20661  dchrvmasumlem2  20663  dchrvmasumiflem2  20667  dchrisum0lem1  20681  dchrisum0lem2  20683  mulog2sumlem2  20700  chpdifbndlem1  20718  selberg3lem1  20722  selberg4lem1  20725  selberg34r  20736  pntrlog2bndlem3  20744  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntlemh  20764  pntlemr  20767  pntlemf  20770  pntlemk  20771  pntlemo  20772  ipasslem4  21428  minvecolem2  21470  his35  21683  leopnmid  22734  subfacval2  23733  subfaclim  23734  circum  24022  faclimlem8  24124  faclimlem9  24125  colinearalglem4  24609  axpasch  24641  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  axcontlem8  24671  bpolydiflem  24861  bpoly4  24866  itgmulc2nc  25019  dvreasin  25026  areacirclem2  25028  areacirclem5  25032  mulmulvec  25790  csbrn  26565  bfplem1  26649  pellexlem6  27022  rmxluc  27124  rmyluc2  27126  rmydbl  27128  jm2.18  27184  jm2.23  27192  jm2.27c  27203  jm3.1lem2  27214  proot1ex  27623  itgsinexplem1  27851  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  wallispi2lem2  27924  stirlinglem3  27928  stirlinglem10  27935  stirlinglem15  27940  sigarls  27950  sharhght  27958
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulass 8819
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator