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

Theorem mulcomi 9392
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 9368 . 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 1369    e. wcel 1756  (class class class)co 6091   CCcc 9280    x. cmul 9287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 9346
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mulcomli  9393  divmul13i  10092  mvllmuli  10164  8th4div3  10545  numma2c  10788  nummul2c  10792  binom2i  11975  binom2aiOLD  11976  fac3  12058  tanval2  13417  pockthi  13968  mod2xnegi  14100  decexp2  14104  decsplit1  14111  decsplit  14112  83prm  14150  dvsincos  21453  sincosq4sgn  21963  ang180lem3  22207  mcubic  22242  cubic2  22243  log2ublem2  22342  log2ublem3  22343  log2ub  22344  basellem8  22425  ppiub  22543  chtub  22551  bposlem8  22630  ax5seglem7  23181  ipdirilem  24229  siilem1  24251  bcseqi  24522  h1de2i  24956  signswch  26962  problem4  27301  problem5  27302  quad3  27303  arearect  29591  areaquad  29592  wallispilem4  29863  zlmodzxzequap  31041
  Copyright terms: Public domain W3C validator