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

Theorem mulassi 9510
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 9485 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  x.  B
)  x.  C )  =  ( A  x.  ( B  x.  C
) ) )
51, 2, 3, 4mp3an 1315 1  |-  ( ( A  x.  B )  x.  C )  =  ( A  x.  ( B  x.  C )
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    e. wcel 1758  (class class class)co 6203   CCcc 9395    x. cmul 9402
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 9463
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  8th4div3  10660  numma  10901  decbin0  10973  faclbnd4lem1  12190  ef01bndlem  13590  dec5dvds  14215  karatsuba  14235  2exp6  14237  sincos4thpi  22118  sincos6thpi  22120  ang180lem2  22349  ang180lem3  22350  asin1  22432  efiatan2  22455  2efiatan  22456  log2cnv  22482  log2ublem2  22485  log2ublem3  22486  log2ub  22487  bclbnd  22762  bposlem8  22773  ax5seglem7  23360  ipasslem10  24418  siilem1  24430  normlem0  24690  normlem9  24699  bcseqi  24701  polid2i  24738  quad3  27470
  Copyright terms: Public domain W3C validator