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

Theorem mulcom 8839
Description: Alias for ax-mulcom 8817, for naming consistency with mulcomi 8859. (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 8817 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 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    x. cmul 8758
This theorem is referenced by:  adddir  8846  mulid2  8852  mulcomi  8859  mulcomd  8872  mul12  8994  mul32  8995  mul31  8996  mul01  9007  muladd  9228  subdir  9230  mulneg2  9233  recextlem1  9414  divmul3  9445  div23  9459  div13  9461  div12  9462  divcan4  9465  divmul13  9479  divmul24  9480  divcan7  9485  div2neg  9499  prodgt02  9618  prodge02  9620  ltmul2  9623  lemul2  9625  lemul2a  9627  ltmulgt12  9633  lemulge12  9635  ltmuldiv2  9643  ltdivmul2  9647  lt2mul2div  9648  ledivmul2  9649  ledivmul2OLD  9650  lemuldiv2  9652  supmul  9738  times2  9860  modcyc  11015  modcyc2  11016  subsq  11226  cjmulrcl  11645  imval2  11652  abscj  11780  sqabsadd  11783  sqabssub  11784  sqreulem  11859  iseraltlem2  12171  iseraltlem3  12172  climcndslem2  12325  efcllem  12375  efexp  12397  sinmul  12468  demoivreALT  12497  dvdsmul1  12566  odd2np1lem  12602  odd2np1  12603  modgcd  12731  bezoutlem1  12733  dvdsgcd  12738  gcdmultiple  12745  coprmdvds  12797  coprmdvds2  12798  qredeq  12801  eulerthlem2  12866  coprimeprodsq2  12879  opeo  12882  omeo  12883  prmreclem6  12984  odmod  14877  cncrng  16411  cnsrng  16424  pcoass  18538  dvlipcn  19357  plydivlem4  19692  quotcan  19705  aaliou3lem3  19740  ef2kpi  19862  sinperlem  19864  sinmpi  19871  cosmpi  19872  sinppi  19873  cosppi  19874  sineq0  19905  tanregt0  19917  logneg  19957  lognegb  19959  logimul  19984  tanarg  19986  logtayl  20023  cxpsqrlem  20065  cubic2  20160  quart1  20168  log2cnv  20256  basellem1  20334  basellem3  20336  basellem5  20338  basellem8  20341  mumul  20435  chtublem  20466  perfectlem1  20484  perfectlem2  20485  perfect  20486  dchrabl  20509  bposlem6  20544  bposlem9  20547  lgsdir2lem4  20581  lgsdir2  20583  lgsdir  20585  lgsdi  20587  lgsquadlem2  20610  lgsquad2  20615  rpvmasum2  20677  mulog2sumlem1  20699  pntibndlem2  20756  pntibndlem3  20757  pntlemf  20770  ablomul  21038  nvscom  21203  ipasslem11  21434  ipblnfi  21450  hvmulcom  21638  h1de2bi  22149  homul12  22401  riesz3i  22658  riesz1  22661  kbass4  22715  mulcan2g  24100  prodmolem3  24156  bpoly3  24864  fsumcube  24866  zintdom  25540  heiborlem6  26642  rmym1  27122  expgrowthi  27652  expgrowth  27654  stoweidlem1  27852  stoweidlem10  27861  stoweidlem11  27862  stoweidlem26  27877  stoweidlem32  27883
This theorem was proved from axioms:  ax-mulcom 8817
  Copyright terms: Public domain W3C validator