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

Theorem mulcomli 8844
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 8843 . 2  |-  ( B  x.  A )  =  ( A  x.  B
)
4 mulcomli.3 . 2  |-  ( A  x.  B )  =  C
53, 4eqtri 2303 1  |-  ( B  x.  A )  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    x. cmul 8742
This theorem is referenced by:  divcan1i  9504  recgt0ii  9662  nummul2c  10161  cos2bnd  12468  dec5nprm  13081  decexp2  13090  karatsuba  13099  2exp8  13102  2exp16  13103  7prm  13112  13prm  13117  17prm  13118  19prm  13119  23prm  13120  43prm  13123  83prm  13124  139prm  13125  163prm  13126  317prm  13127  631prm  13128  1259lem1  13129  1259lem2  13130  1259lem3  13131  1259lem4  13132  1259lem5  13133  1259prm  13134  2503lem1  13135  2503lem2  13136  2503lem3  13137  2503prm  13138  4001lem1  13139  4001lem2  13140  4001lem3  13141  4001lem4  13142  4001prm  13143  pcoass  18522  efif1olem2  19905  mcubic  20143  quart1lem  20151  quart1  20152  quartlem1  20153  tanatan  20215  log2ublem3  20244  log2ub  20245  cht3  20411  bclbnd  20519  bpos1lem  20521  bposlem4  20526  bposlem5  20527  bposlem8  20530  ipasslem10  21417  siii  21431  normlem3  21691  bcsiALT  21758  halfthird  24100  5recm6rec  24101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264  ax-mulcom 8801
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276
  Copyright terms: Public domain W3C validator