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

Theorem mulcomli 9602
Description: Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1  |-  A  e.  CC
axi.2  |-  B  e.  CC
mulcomli.3  |-  ( A  x.  B )  =  C
Assertion
Ref Expression
mulcomli  |-  ( B  x.  A )  =  C

Proof of Theorem mulcomli
StepHypRef Expression
1 axi.2 . . 3  |-  B  e.  CC
2 axi.1 . . 3  |-  A  e.  CC
31, 2mulcomi 9601 . 2  |-  ( B  x.  A )  =  ( A  x.  B
)
4 mulcomli.3 . 2  |-  ( A  x.  B )  =  C
53, 4eqtri 2496 1  |-  ( B  x.  A )  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    e. wcel 1767  (class class class)co 6283   CCcc 9489    x. cmul 9496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445  ax-mulcom 9555
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459
This theorem is referenced by:  divcan1i  10287  recgt0ii  10450  nummul2c  11012  cos2bnd  13783  dec5nprm  14410  decexp2  14419  karatsuba  14428  2exp8  14431  2exp16  14432  7prm  14453  13prm  14458  17prm  14459  19prm  14460  23prm  14461  43prm  14464  83prm  14465  139prm  14466  163prm  14467  317prm  14468  631prm  14469  1259lem1  14470  1259lem2  14471  1259lem3  14472  1259lem4  14473  1259lem5  14474  1259prm  14475  2503lem1  14476  2503lem2  14477  2503lem3  14478  2503prm  14479  4001lem1  14480  4001lem2  14481  4001lem3  14482  4001lem4  14483  4001prm  14484  pcoass  21275  efif1olem2  22679  mcubic  22922  quart1lem  22930  quart1  22931  quartlem1  22932  tanatan  22994  log2ublem3  23023  log2ub  23024  cht3  23191  bclbnd  23299  bpos1lem  23301  bposlem4  23306  bposlem5  23307  bposlem8  23310  ipasslem10  25446  siii  25460  normlem3  25721  bcsiALT  25788  halfthird  28604  5recm6rec  28605  fouriersw  31548
  Copyright terms: Public domain W3C validator