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

Theorem mulcom 9032
Description: Alias for ax-mulcom 9010, for naming consistency with mulcomi 9052. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
mulcom  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )

Proof of Theorem mulcom
StepHypRef Expression
1 ax-mulcom 9010 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649    e. wcel 1721  (class class class)co 6040   CCcc 8944    x. cmul 8951
This theorem is referenced by:  adddir  9039  mulid2  9045  mulcomi  9052  mulcomd  9065  mul12  9188  mul32  9189  mul31  9190  mul01  9201  muladd  9422  subdir  9424  mulneg2  9427  recextlem1  9608  divmul3  9639  div23  9653  div13  9655  div12  9656  divcan4  9659  divmul13  9673  divmul24  9674  divcan7  9679  div2neg  9693  prodgt02  9812  prodge02  9814  ltmul2  9817  lemul2  9819  lemul2a  9821  ltmulgt12  9827  lemulge12  9829  ltmuldiv2  9837  ltdivmul2  9841  lt2mul2div  9842  ledivmul2  9843  ledivmul2OLD  9844  lemuldiv2  9846  supmul  9932  times2  10056  modcyc  11231  modcyc2  11232  subsq  11443  cjmulrcl  11904  imval2  11911  abscj  12039  sqabsadd  12042  sqabssub  12043  sqreulem  12118  iseraltlem2  12431  iseraltlem3  12432  climcndslem2  12585  efcllem  12635  efexp  12657  sinmul  12728  demoivreALT  12757  dvdsmul1  12826  odd2np1lem  12862  odd2np1  12863  modgcd  12991  bezoutlem1  12993  dvdsgcd  12998  gcdmultiple  13005  coprmdvds  13057  coprmdvds2  13058  qredeq  13061  eulerthlem2  13126  coprimeprodsq2  13139  opeo  13142  omeo  13143  prmreclem6  13244  odmod  15139  cncrng  16677  cnsrng  16690  pcoass  19002  dvlipcn  19831  plydivlem4  20166  quotcan  20179  aaliou3lem3  20214  ef2kpi  20339  sinperlem  20341  sinmpi  20348  cosmpi  20349  sinppi  20350  cosppi  20351  sineq0  20382  tanregt0  20394  logneg  20435  lognegb  20437  logimul  20462  tanarg  20467  logtayl  20504  cxpsqrlem  20546  cubic2  20641  quart1  20649  log2cnv  20737  basellem1  20816  basellem3  20818  basellem5  20820  basellem8  20823  mumul  20917  chtublem  20948  perfectlem1  20966  perfectlem2  20967  perfect  20968  dchrabl  20991  bposlem6  21026  bposlem9  21029  lgsdir2lem4  21063  lgsdir2  21065  lgsdir  21067  lgsdi  21069  lgsquadlem2  21092  lgsquad2  21097  rpvmasum2  21159  mulog2sumlem1  21181  pntibndlem2  21238  pntibndlem3  21239  pntlemf  21252  ablomul  21896  nvscom  22063  ipasslem11  22294  ipblnfi  22310  hvmulcom  22498  h1de2bi  23009  homul12  23261  riesz3i  23518  riesz1  23521  kbass4  23575  mulcan2g  25143  prodfmul  25171  prodmolem3  25212  bpoly3  26008  heiborlem6  26415  rmym1  26888  expgrowthi  27418  expgrowth  27420  stoweidlem10  27626
This theorem was proved from axioms:  ax-mulcom 9010
  Copyright terms: Public domain W3C validator