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

Theorem mulcomi 8843
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 8823 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3mp2an 653 1  |-  ( A  x.  B )  =  ( B  x.  A
)
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:  mulcomli  8844  divmul13i  9521  8th4div3  9935  numma2c  10157  nummul2c  10161  binom2i  11212  binom2aiOLD  11213  fac3  11295  tanval2  12413  pockthi  12954  mod2xnegi  13086  decexp2  13090  decsplit1  13097  decsplit  13098  83prm  13124  dvsincos  19328  sincosq4sgn  19869  ang180lem3  20109  mcubic  20143  cubic2  20144  log2ublem2  20243  log2ublem3  20244  log2ub  20245  basellem8  20325  ppiub  20443  chtub  20451  bposlem8  20530  ipdirilem  21407  siilem1  21429  bcseqi  21699  h1de2i  22132  ax5seglem7  24563  wallispilem4  27817
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcom 8801
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator