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

Theorem mulcomli 9097
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 9096 . 2  |-  ( B  x.  A )  =  ( A  x.  B
)
4 mulcomli.3 . 2  |-  ( A  x.  B )  =  C
53, 4eqtri 2456 1  |-  ( B  x.  A )  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725  (class class class)co 6081   CCcc 8988    x. cmul 8995
This theorem is referenced by:  divcan1i  9758  recgt0ii  9916  nummul2c  10419  cos2bnd  12789  dec5nprm  13402  decexp2  13411  karatsuba  13420  2exp8  13423  2exp16  13424  7prm  13433  13prm  13438  17prm  13439  19prm  13440  23prm  13441  43prm  13444  83prm  13445  139prm  13446  163prm  13447  317prm  13448  631prm  13449  1259lem1  13450  1259lem2  13451  1259lem3  13452  1259lem4  13453  1259lem5  13454  1259prm  13455  2503lem1  13456  2503lem2  13457  2503lem3  13458  2503prm  13459  4001lem1  13460  4001lem2  13461  4001lem3  13462  4001lem4  13463  4001prm  13464  pcoass  19049  efif1olem2  20445  mcubic  20687  quart1lem  20695  quart1  20696  quartlem1  20697  tanatan  20759  log2ublem3  20788  log2ub  20789  cht3  20956  bclbnd  21064  bpos1lem  21066  bposlem4  21071  bposlem5  21072  bposlem8  21075  ipasslem10  22340  siii  22354  normlem3  22614  bcsiALT  22681  halfthird  25205  5recm6rec  25206
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417  ax-mulcom 9054
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator