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

Theorem mulcomi 9632
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 9608 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3mp2an 670 1  |-  ( A  x.  B )  =  ( B  x.  A
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405    e. wcel 1842  (class class class)co 6278   CCcc 9520    x. cmul 9527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulcom 9586
This theorem depends on definitions:  df-bi 185  df-an 369
This theorem is referenced by:  mulcomli  9633  divmul13i  10346  8th4div3  10800  numma2c  11052  nummul2c  11056  binom2i  12322  fac3  12404  tanval2  14077  pockthi  14634  mod2xnegi  14766  decexp2  14770  decsplit1  14777  decsplit  14778  83prm  14817  dvsincos  22674  sincosq4sgn  23186  ang180lem3  23470  mcubic  23503  cubic2  23504  log2ublem2  23603  log2ublem3  23604  log2ub  23605  basellem8  23742  ppiub  23860  chtub  23868  bposlem8  23947  ax5seglem7  24655  ex-ind-dvds  25587  ipdirilem  26158  siilem1  26180  bcseqi  26451  h1de2i  26885  signswch  29024  problem4  29874  problem5  29875  quad3  29876  arearect  35547  areaquad  35548  wallispilem4  37218  dirkercncflem1  37253  fourierswlem  37381  5tcu2e40  37861  41prothprm  37865  zlmodzxzequap  38611
  Copyright terms: Public domain W3C validator