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

Theorem mulcom 8913
Description: Alias for ax-mulcom 8891, for naming consistency with mulcomi 8933. (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 8891 1  |-  ( ( A  e.  CC  /\  B  e.  CC )  ->  ( A  x.  B
)  =  ( B  x.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1642    e. wcel 1710  (class class class)co 5945   CCcc 8825    x. cmul 8832
This theorem is referenced by:  adddir  8920  mulid2  8926  mulcomi  8933  mulcomd  8946  mul12  9068  mul32  9069  mul31  9070  mul01  9081  muladd  9302  subdir  9304  mulneg2  9307  recextlem1  9488  divmul3  9519  div23  9533  div13  9535  div12  9536  divcan4  9539  divmul13  9553  divmul24  9554  divcan7  9559  div2neg  9573  prodgt02  9692  prodge02  9694  ltmul2  9697  lemul2  9699  lemul2a  9701  ltmulgt12  9707  lemulge12  9709  ltmuldiv2  9717  ltdivmul2  9721  lt2mul2div  9722  ledivmul2  9723  ledivmul2OLD  9724  lemuldiv2  9726  supmul  9812  times2  9936  modcyc  11091  modcyc2  11092  subsq  11303  cjmulrcl  11725  imval2  11732  abscj  11860  sqabsadd  11863  sqabssub  11864  sqreulem  11939  iseraltlem2  12252  iseraltlem3  12253  climcndslem2  12406  efcllem  12456  efexp  12478  sinmul  12549  demoivreALT  12578  dvdsmul1  12647  odd2np1lem  12683  odd2np1  12684  modgcd  12812  bezoutlem1  12814  dvdsgcd  12819  gcdmultiple  12826  coprmdvds  12878  coprmdvds2  12879  qredeq  12882  eulerthlem2  12947  coprimeprodsq2  12960  opeo  12963  omeo  12964  prmreclem6  13065  odmod  14960  cncrng  16501  cnsrng  16514  pcoass  18626  dvlipcn  19445  plydivlem4  19780  quotcan  19793  aaliou3lem3  19828  ef2kpi  19953  sinperlem  19955  sinmpi  19962  cosmpi  19963  sinppi  19964  cosppi  19965  sineq0  19996  tanregt0  20008  logneg  20049  lognegb  20051  logimul  20076  tanarg  20081  logtayl  20118  cxpsqrlem  20160  cubic2  20255  quart1  20263  log2cnv  20351  basellem1  20430  basellem3  20432  basellem5  20434  basellem8  20437  mumul  20531  chtublem  20562  perfectlem1  20580  perfectlem2  20581  perfect  20582  dchrabl  20605  bposlem6  20640  bposlem9  20643  lgsdir2lem4  20677  lgsdir2  20679  lgsdir  20681  lgsdi  20683  lgsquadlem2  20706  lgsquad2  20711  rpvmasum2  20773  mulog2sumlem1  20795  pntibndlem2  20852  pntibndlem3  20853  pntlemf  20866  ablomul  21134  nvscom  21301  ipasslem11  21532  ipblnfi  21548  hvmulcom  21736  h1de2bi  22247  homul12  22499  riesz3i  22756  riesz1  22759  kbass4  22813  mulcan2g  24491  prodfmul  24519  prodmolem3  24560  bpoly3  25352  fsumcube  25354  heiborlem6  25863  rmym1  26343  expgrowthi  26873  expgrowth  26875  stoweidlem1  27073  stoweidlem10  27082  stoweidlem11  27083  stoweidlem26  27098  stoweidlem32  27104
This theorem was proved from axioms:  ax-mulcom 8891
  Copyright terms: Public domain W3C validator