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

Theorem mulcomli 8860
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 8859 . 2  |-  ( B  x.  A )  =  ( A  x.  B
)
4 mulcomli.3 . 2  |-  ( A  x.  B )  =  C
53, 4eqtri 2316 1  |-  ( B  x.  A )  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    x. cmul 8758
This theorem is referenced by:  divcan1i  9520  recgt0ii  9678  nummul2c  10177  cos2bnd  12484  dec5nprm  13097  decexp2  13106  karatsuba  13115  2exp8  13118  2exp16  13119  7prm  13128  13prm  13133  17prm  13134  19prm  13135  23prm  13136  43prm  13139  83prm  13140  139prm  13141  163prm  13142  317prm  13143  631prm  13144  1259lem1  13145  1259lem2  13146  1259lem3  13147  1259lem4  13148  1259lem5  13149  1259prm  13150  2503lem1  13151  2503lem2  13152  2503lem3  13153  2503prm  13154  4001lem1  13155  4001lem2  13156  4001lem3  13157  4001lem4  13158  4001prm  13159  pcoass  18538  efif1olem2  19921  mcubic  20159  quart1lem  20167  quart1  20168  quartlem1  20169  tanatan  20231  log2ublem3  20260  log2ub  20261  cht3  20427  bclbnd  20535  bpos1lem  20537  bposlem4  20542  bposlem5  20543  bposlem8  20546  ipasslem10  21433  siii  21447  normlem3  21707  bcsiALT  21774  halfthird  24115  5recm6rec  24116
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277  ax-mulcom 8817
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289
  Copyright terms: Public domain W3C validator