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

Theorem mulassd 8858
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 8825 . 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 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    x. cmul 8742
This theorem is referenced by:  recex  9400  mulcand  9401  receu  9413  divdivdiv  9461  divmuleq  9465  conjmul  9477  modmul1  11002  moddi  11007  expadd  11144  binom3  11222  digit1  11235  discr1  11237  discr  11238  faclbnd  11303  faclbnd6  11312  bcm1k  11327  bcp1nk  11329  crre  11599  remullem  11613  amgm2  11853  iseraltlem2  12155  iseraltlem3  12156  binomlem  12287  climcndslem2  12309  geo2sum  12329  mertenslem1  12340  sinadd  12444  tanadd  12447  bezoutlem3  12719  dvdsmulgcd  12733  qredeq  12785  pcaddlem  12936  prmpwdvds  12951  ablfacrp  15301  nmoco  18246  cph2ass  18648  minveclem2  18790  uniioombllem5  18942  itg1mulc  19059  mbfi1fseqlem5  19074  itgconst  19173  itgmulc2  19188  dvexp  19302  dvply1  19664  elqaalem3  19701  aalioulem1  19712  aaliou3lem2  19723  dvtaylp  19749  dvradcnv  19797  pserdvlem2  19804  tangtx  19873  tanregt0  19901  tanarg  19970  logcnlem4  19992  cxpmul  20035  dvcxp1  20082  root1eq1  20095  quad2  20135  dcubic1lem  20139  dcubic1  20141  cubic2  20144  binom4  20146  dquartlem1  20147  dquartlem2  20148  dquart  20149  quart1lem  20151  quart1  20152  quartlem1  20153  efiasin  20184  asinsinlem  20187  asinsin  20188  efiatan  20208  efiatan2  20213  2efiatan  20214  atantan  20219  atanbndlem  20221  atans2  20227  atantayl  20233  log2cnv  20240  log2tlbnd  20241  ftalem1  20310  ftalem5  20314  basellem3  20320  basellem5  20322  basellem8  20325  chtub  20451  perfectlem1  20468  perfectlem2  20469  perfect  20470  bcmono  20516  bclbnd  20519  bposlem9  20531  lgsneg  20558  lgseisenlem1  20588  lgseisenlem2  20589  lgseisenlem3  20590  lgseisenlem4  20591  lgsquad2lem1  20597  lgsquad3  20600  2sqlem3  20605  chto1ub  20625  rplogsumlem1  20633  dchrmusum2  20643  dchrvmasum2lem  20645  dchrvmasumlem2  20647  dchrvmasumiflem2  20651  dchrisum0lem1  20665  dchrisum0lem2  20667  mulog2sumlem2  20684  chpdifbndlem1  20702  selberg3lem1  20706  selberg4lem1  20709  selberg34r  20720  pntrlog2bndlem3  20728  pntrlog2bndlem5  20730  pntrlog2bndlem6  20732  pntlemh  20748  pntlemr  20751  pntlemf  20754  pntlemk  20755  pntlemo  20756  ipasslem4  21412  minvecolem2  21454  his35  21667  leopnmid  22718  subfacval2  23129  subfaclim  23130  circum  23418  colinearalglem4  23948  axpasch  23980  axcontlem2  24004  axcontlem4  24006  axcontlem7  24009  axcontlem8  24010  bpolydiflem  24200  bpoly4  24205  dvreasin  24334  areacirclem2  24337  areacirclem5  24341  mulmulvec  25099  csbrn  25874  bfplem1  25958  pellexlem6  26331  rmxluc  26433  rmyluc2  26435  rmydbl  26437  jm2.18  26493  jm2.23  26501  jm2.27c  26512  jm3.1lem2  26523  proot1ex  26932  itgsinexplem1  27160  wallispilem5  27230  wallispi  27231  wallispi2lem1  27232  wallispi2lem2  27233  stirlinglem3  27237  stirlinglem10  27244  stirlinglem15  27249  sigarls  27259  sharhght  27267
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulass 8803
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator