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

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

Proof of Theorem mulcomi
StepHypRef Expression
1 axi.1 . 2  |-  A  e.  CC
2 axi.2 . 2  |-  B  e.  CC
3 mulcom 9574 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3mp2an 672 1  |-  ( A  x.  B )  =  ( B  x.  A
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    e. wcel 1767  (class class class)co 6282   CCcc 9486    x. cmul 9493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 9552
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mulcomli  9599  divmul13i  10301  mvllmuli  10373  8th4div3  10755  numma2c  11005  nummul2c  11009  binom2i  12239  binom2aiOLD  12240  fac3  12322  tanval2  13722  pockthi  14277  mod2xnegi  14409  decexp2  14413  decsplit1  14420  decsplit  14421  83prm  14459  dvsincos  22114  sincosq4sgn  22624  ang180lem3  22868  mcubic  22903  cubic2  22904  log2ublem2  23003  log2ublem3  23004  log2ub  23005  basellem8  23086  ppiub  23204  chtub  23212  bposlem8  23291  ax5seglem7  23911  ipdirilem  25417  siilem1  25439  bcseqi  25710  h1de2i  26144  signswch  28155  problem4  28494  problem5  28495  quad3  28496  arearect  30788  areaquad  30789  wallispilem4  31368  dirkercncflem1  31403  fourierswlem  31531  zlmodzxzequap  32181
  Copyright terms: Public domain W3C validator