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

Theorem mulassi 8846
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 8825 . 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 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    x. cmul 8742
This theorem is referenced by:  8th4div3  9935  numma  10155  decbin0  10227  faclbnd4lem1  11306  ef01bndlem  12464  dec5dvds  13079  karatsuba  13099  2exp6  13101  sincos4thpi  19881  sincos6thpi  19883  ang180lem2  20108  ang180lem3  20109  asin1  20190  efiatan2  20213  2efiatan  20214  log2cnv  20240  log2ublem2  20243  log2ublem3  20244  log2ub  20245  bclbnd  20519  bposlem8  20530  ipasslem10  21417  siilem1  21429  normlem0  21688  normlem9  21697  bcseqi  21699  polid2i  21736  ax5seglem7  24563
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