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

Theorem mulcomi 9651
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 9627 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3mp2an 677 1  |-  ( A  x.  B )  =  ( B  x.  A
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1438    e. wcel 1869  (class class class)co 6303   CCcc 9539    x. cmul 9546
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 9605
This theorem depends on definitions:  df-bi 189  df-an 373
This theorem is referenced by:  mulcomli  9652  divmul13i  10370  8th4div3  10835  numma2c  11086  nummul2c  11090  binom2i  12385  fac3  12467  tanval2  14180  pockthi  14844  mod2xnegi  15036  decexp2  15040  decsplit1  15047  decsplit  15048  83prm  15087  dvsincos  22925  sincosq4sgn  23448  ang180lem3  23732  mcubic  23765  cubic2  23766  log2ublem2  23865  log2ublem3  23866  log2ub  23867  basellem8  24006  ppiub  24124  chtub  24132  bposlem8  24211  ax5seglem7  24957  ex-ind-dvds  25891  ipdirilem  26462  siilem1  26484  bcseqi  26765  h1de2i  27198  signswch  29452  problem4  30302  problem5  30303  quad3  30304  arearect  36064  areaquad  36065  wallispilem4  37794  dirkercncflem1  37829  fourierswlem  37958  tgoldbachlt  38665  5tcu2e40  38671  41prothprm  38675  zlmodzxzequap  39636
  Copyright terms: Public domain W3C validator