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

Theorem mulassi 9626
 Description: Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1
axi.2
axi.3
Assertion
Ref Expression
mulassi

Proof of Theorem mulassi
StepHypRef Expression
1 axi.1 . 2
2 axi.2 . 2
3 axi.3 . 2
4 mulass 9601 . 2
51, 2, 3, 4mp3an 1324 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395  e.wcel 1818  (class class class)co 6296   cc 9511   cmul 9518 This theorem is referenced by:  8th4div3  10784  numma  11035  decbin0  11107  faclbnd4lem1  12371  ef01bndlem  13919  dec5dvds  14550  karatsuba  14570  2exp6OLD  14573  sincos4thpi  22906  sincos6thpi  22908  ang180lem2  23142  ang180lem3  23143  asin1  23225  efiatan2  23248  2efiatan  23249  log2cnv  23275  log2ublem2  23278  log2ublem3  23279  log2ub  23280  bclbnd  23555  bposlem8  23566  ax5seglem7  24238  ipasslem10  25754  siilem1  25766  normlem0  26026  normlem9  26035  bcseqi  26037  polid2i  26074  quad3  29024  iexpire  29122  fourierswlem  32013  fouriersw  32014 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 9579 This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
 Copyright terms: Public domain W3C validator