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

Theorem mulassi 9617
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 9592 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
51, 2, 3, 4mp3an 1324 1  |-  ( ( A  x.  B )  x.  C )  =  ( A  x.  ( B  x.  C )
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    e. wcel 1767  (class class class)co 6295   CCcc 9502    x. cmul 9509
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 9570
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  8th4div3  10771  numma  11019  decbin0  11091  faclbnd4lem1  12351  ef01bndlem  13797  dec5dvds  14426  karatsuba  14446  2exp6  14448  sincos4thpi  22772  sincos6thpi  22774  ang180lem2  23008  ang180lem3  23009  asin1  23091  efiatan2  23114  2efiatan  23115  log2cnv  23141  log2ublem2  23144  log2ublem3  23145  log2ub  23146  bclbnd  23421  bposlem8  23432  ax5seglem7  24061  ipasslem10  25577  siilem1  25589  normlem0  25849  normlem9  25858  bcseqi  25860  polid2i  25897  quad3  28849  fourierswlem  31854  fouriersw  31855
  Copyright terms: Public domain W3C validator