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

Theorem mulcomi 9097
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 9077 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
41, 2, 3mp2an 655 1  |-  ( A  x.  B )  =  ( B  x.  A
)
Colors of variables: wff set class
Syntax hints:    = wceq 1653    e. wcel 1726  (class class class)co 6082   CCcc 8989    x. cmul 8996
This theorem is referenced by:  mulcomli  9098  divmul13i  9776  8th4div3  10192  numma2c  10416  nummul2c  10420  binom2i  11491  binom2aiOLD  11492  fac3  11574  tanval2  12735  pockthi  13276  mod2xnegi  13408  decexp2  13412  decsplit1  13419  decsplit  13420  83prm  13446  dvsincos  19866  sincosq4sgn  20410  ang180lem3  20654  mcubic  20688  cubic2  20689  log2ublem2  20788  log2ublem3  20789  log2ub  20790  basellem8  20871  ppiub  20989  chtub  20997  bposlem8  21076  ipdirilem  22331  siilem1  22353  bcseqi  22623  h1de2i  23056  ax5seglem7  25875  wallispilem4  27794
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-mulcom 9055
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator