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  23718  subfaclim  23719  circum  24007  colinearalglem4  24537  axpasch  24569  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  bpolydiflem  24789  bpoly4  24794  dvreasin  24923  areacirclem2  24925  areacirclem5  24929  mulmulvec  25687  csbrn  26462  bfplem1  26546  pellexlem6  26919  rmxluc  27021  rmyluc2  27023  rmydbl  27025  jm2.18  27081  jm2.23  27089  jm2.27c  27100  jm3.1lem2  27111  proot1ex  27520  itgsinexplem1  27748  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2lem2  27821  stirlinglem3  27825  stirlinglem10  27832  stirlinglem15  27837  sigarls  27847  sharhght  27855
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