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
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 9592 . 2
51, 2, 3, 4mp3an 1324 1
 Colors of variables: wff setvar class Syntax hints:   wceq 1379   wcel 1767  (class class class)co 6295  cc 9502   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