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

Theorem mulassi 9383
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 9358 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
51, 2, 3, 4mp3an 1307 1  |-  ( ( A  x.  B )  x.  C )  =  ( A  x.  ( B  x.  C )
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362    e. wcel 1755  (class class class)co 6080   CCcc 9268    x. cmul 9275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 9336
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 960
This theorem is referenced by:  8th4div3  10533  numma  10774  decbin0  10846  faclbnd4lem1  12053  ef01bndlem  13451  dec5dvds  14076  karatsuba  14096  2exp6  14098  sincos4thpi  21860  sincos6thpi  21862  ang180lem2  22091  ang180lem3  22092  asin1  22174  efiatan2  22197  2efiatan  22198  log2cnv  22224  log2ublem2  22227  log2ublem3  22228  log2ub  22229  bclbnd  22504  bposlem8  22515  ax5seglem7  23004  ipasslem10  24062  siilem1  24074  normlem0  24334  normlem9  24343  bcseqi  24345  polid2i  24382
  Copyright terms: Public domain W3C validator