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

Theorem mulassi 8936
Description: Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1  |-  A  e.  CC
axi.2  |-  B  e.  CC
axi.3  |-  C  e.  CC
Assertion
Ref Expression
mulassi  |-  ( ( A  x.  B )  x.  C )  =  ( A  x.  ( B  x.  C )
)

Proof of Theorem mulassi
StepHypRef Expression
1 axi.1 . 2  |-  A  e.  CC
2 axi.2 . 2  |-  B  e.  CC
3 axi.3 . 2  |-  C  e.  CC
4 mulass 8915 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
51, 2, 3, 4mp3an 1277 1  |-  ( ( A  x.  B )  x.  C )  =  ( A  x.  ( B  x.  C )
)
Colors of variables: wff set class
Syntax hints:    = wceq 1642    e. wcel 1710  (class class class)co 5945   CCcc 8825    x. cmul 8832
This theorem is referenced by:  8th4div3  10027  numma  10247  decbin0  10319  faclbnd4lem1  11399  ef01bndlem  12561  dec5dvds  13176  karatsuba  13196  2exp6  13198  sincos4thpi  19988  sincos6thpi  19990  ang180lem2  20219  ang180lem3  20220  asin1  20301  efiatan2  20324  2efiatan  20325  log2cnv  20351  log2ublem2  20354  log2ublem3  20355  log2ub  20356  bclbnd  20631  bposlem8  20642  ipasslem10  21531  siilem1  21543  normlem0  21802  normlem9  21811  bcseqi  21813  polid2i  21850  ax5seglem7  25122
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulass 8893
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator