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

Theorem mulassi 9063
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 9042 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
51, 2, 3, 4mp3an 1279 1  |-  ( ( A  x.  B )  x.  C )  =  ( A  x.  ( B  x.  C )
)
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721  (class class class)co 6048   CCcc 8952    x. cmul 8959
This theorem is referenced by:  8th4div3  10155  numma  10377  decbin0  10449  faclbnd4lem1  11547  ef01bndlem  12748  dec5dvds  13363  karatsuba  13383  2exp6  13385  sincos4thpi  20382  sincos6thpi  20384  ang180lem2  20613  ang180lem3  20614  asin1  20695  efiatan2  20718  2efiatan  20719  log2cnv  20745  log2ublem2  20748  log2ublem3  20749  log2ub  20750  bclbnd  21025  bposlem8  21036  ipasslem10  22301  siilem1  22313  normlem0  22572  normlem9  22581  bcseqi  22583  polid2i  22620  ax5seglem7  25786
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulass 9020
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator