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

Theorem mulcomi 8859
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 8839 . 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 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    x. cmul 8758
This theorem is referenced by:  mulcomli  8860  divmul13i  9537  8th4div3  9951  numma2c  10173  nummul2c  10177  binom2i  11228  binom2aiOLD  11229  fac3  11311  tanval2  12429  pockthi  12970  mod2xnegi  13102  decexp2  13106  decsplit1  13113  decsplit  13114  83prm  13140  dvsincos  19344  sincosq4sgn  19885  ang180lem3  20125  mcubic  20159  cubic2  20160  log2ublem2  20259  log2ublem3  20260  log2ub  20261  basellem8  20341  ppiub  20459  chtub  20467  bposlem8  20546  ipdirilem  21423  siilem1  21445  bcseqi  21715  h1de2i  22148  ax5seglem7  24635  wallispilem4  27920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcom 8817
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator