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

Theorem mulcom 9002
Description: Alias for ax-mulcom 8980, for naming consistency with mulcomi 9022. (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 8980 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 1717  (class class class)co 6013   CCcc 8914    x. cmul 8921
This theorem is referenced by:  adddir  9009  mulid2  9015  mulcomi  9022  mulcomd  9035  mul12  9157  mul32  9158  mul31  9159  mul01  9170  muladd  9391  subdir  9393  mulneg2  9396  recextlem1  9577  divmul3  9608  div23  9622  div13  9624  div12  9625  divcan4  9628  divmul13  9642  divmul24  9643  divcan7  9648  div2neg  9662  prodgt02  9781  prodge02  9783  ltmul2  9786  lemul2  9788  lemul2a  9790  ltmulgt12  9796  lemulge12  9798  ltmuldiv2  9806  ltdivmul2  9810  lt2mul2div  9811  ledivmul2  9812  ledivmul2OLD  9813  lemuldiv2  9815  supmul  9901  times2  10025  modcyc  11196  modcyc2  11197  subsq  11408  cjmulrcl  11869  imval2  11876  abscj  12004  sqabsadd  12007  sqabssub  12008  sqreulem  12083  iseraltlem2  12396  iseraltlem3  12397  climcndslem2  12550  efcllem  12600  efexp  12622  sinmul  12693  demoivreALT  12722  dvdsmul1  12791  odd2np1lem  12827  odd2np1  12828  modgcd  12956  bezoutlem1  12958  dvdsgcd  12963  gcdmultiple  12970  coprmdvds  13022  coprmdvds2  13023  qredeq  13026  eulerthlem2  13091  coprimeprodsq2  13104  opeo  13107  omeo  13108  prmreclem6  13209  odmod  15104  cncrng  16638  cnsrng  16651  pcoass  18913  dvlipcn  19738  plydivlem4  20073  quotcan  20086  aaliou3lem3  20121  ef2kpi  20246  sinperlem  20248  sinmpi  20255  cosmpi  20256  sinppi  20257  cosppi  20258  sineq0  20289  tanregt0  20301  logneg  20342  lognegb  20344  logimul  20369  tanarg  20374  logtayl  20411  cxpsqrlem  20453  cubic2  20548  quart1  20556  log2cnv  20644  basellem1  20723  basellem3  20725  basellem5  20727  basellem8  20730  mumul  20824  chtublem  20855  perfectlem1  20873  perfectlem2  20874  perfect  20875  dchrabl  20898  bposlem6  20933  bposlem9  20936  lgsdir2lem4  20970  lgsdir2  20972  lgsdir  20974  lgsdi  20976  lgsquadlem2  20999  lgsquad2  21004  rpvmasum2  21066  mulog2sumlem1  21088  pntibndlem2  21145  pntibndlem3  21146  pntlemf  21159  ablomul  21784  nvscom  21951  ipasslem11  22182  ipblnfi  22198  hvmulcom  22386  h1de2bi  22897  homul12  23149  riesz3i  23406  riesz1  23409  kbass4  23463  mulcan2g  24962  prodfmul  24990  prodmolem3  25031  bpoly3  25811  heiborlem6  26209  rmym1  26682  expgrowthi  27212  expgrowth  27214  stoweidlem10  27420
This theorem was proved from axioms:  ax-mulcom 8980
  Copyright terms: Public domain W3C validator