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

Theorem mulcom 8823
Description: Alias for ax-mulcom 8801, for naming consistency with mulcomi 8843. (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 8801 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 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    x. cmul 8742
This theorem is referenced by:  adddir  8830  mulid2  8836  mulcomi  8843  mulcomd  8856  mul12  8978  mul32  8979  mul31  8980  mul01  8991  muladd  9212  subdir  9214  mulneg2  9217  recextlem1  9398  divmul3  9429  div23  9443  div13  9445  div12  9446  divcan4  9449  divmul13  9463  divmul24  9464  divcan7  9469  div2neg  9483  prodgt02  9602  prodge02  9604  ltmul2  9607  lemul2  9609  lemul2a  9611  ltmulgt12  9617  lemulge12  9619  ltmuldiv2  9627  ltdivmul2  9631  lt2mul2div  9632  ledivmul2  9633  ledivmul2OLD  9634  lemuldiv2  9636  supmul  9722  times2  9844  modcyc  10999  modcyc2  11000  subsq  11210  cjmulrcl  11629  imval2  11636  abscj  11764  sqabsadd  11767  sqabssub  11768  sqreulem  11843  iseraltlem2  12155  iseraltlem3  12156  climcndslem2  12309  efcllem  12359  efexp  12381  sinmul  12452  demoivreALT  12481  dvdsmul1  12550  odd2np1lem  12586  odd2np1  12587  modgcd  12715  bezoutlem1  12717  dvdsgcd  12722  gcdmultiple  12729  coprmdvds  12781  coprmdvds2  12782  qredeq  12785  eulerthlem2  12850  coprimeprodsq2  12863  opeo  12866  omeo  12867  prmreclem6  12968  odmod  14861  cncrng  16395  cnsrng  16408  pcoass  18522  dvlipcn  19341  plydivlem4  19676  quotcan  19689  aaliou3lem3  19724  ef2kpi  19846  sinperlem  19848  sinmpi  19855  cosmpi  19856  sinppi  19857  cosppi  19858  sineq0  19889  tanregt0  19901  logneg  19941  lognegb  19943  logimul  19968  tanarg  19970  logtayl  20007  cxpsqrlem  20049  cubic2  20144  quart1  20152  log2cnv  20240  basellem1  20318  basellem3  20320  basellem5  20322  basellem8  20325  mumul  20419  chtublem  20450  perfectlem1  20468  perfectlem2  20469  perfect  20470  dchrabl  20493  bposlem6  20528  bposlem9  20531  lgsdir2lem4  20565  lgsdir2  20567  lgsdir  20569  lgsdi  20571  lgsquadlem2  20594  lgsquad2  20599  rpvmasum2  20661  mulog2sumlem1  20683  pntibndlem2  20740  pntibndlem3  20741  pntlemf  20754  ablomul  21022  nvscom  21187  ipasslem11  21418  ipblnfi  21434  hvmulcom  21622  h1de2bi  22133  homul12  22385  riesz3i  22642  riesz1  22645  kbass4  22699  mulcan2g  24085  bpoly3  24793  fsumcube  24795  zintdom  25438  heiborlem6  26540  rmym1  27020  expgrowthi  27550  expgrowth  27552  stoweidlem1  27750  stoweidlem10  27759  stoweidlem11  27760  stoweidlem26  27775  stoweidlem32  27781
This theorem was proved from axioms:  ax-mulcom 8801
  Copyright terms: Public domain W3C validator