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

Theorem mulcom 10060
Description: Alias for ax-mulcom 10038, for naming consistency with mulcomi 10084. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
mulcom ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Proof of Theorem mulcom
StepHypRef Expression
1 ax-mulcom 10038 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  wcel 2030  (class class class)co 6690  cc 9972   · cmul 9979
This theorem was proved from axioms:  ax-mulcom 10038
This theorem is referenced by:  adddir  10069  mulid2  10076  mulcomi  10084  mulcomd  10099  mul12  10240  mul32  10241  mul31  10242  mul01  10253  muladd  10500  subdir  10502  mulneg2  10505  recextlem1  10695  mulcan2g  10719  divmul3  10728  div23  10742  div13  10744  div12  10745  divmulasscom  10747  divcan4  10750  divmul13  10766  divmul24  10767  divcan7  10772  div2neg  10786  prodgt02  10907  prodge02  10909  ltmul2  10912  lemul2  10914  lemul2a  10916  ltmulgt12  10922  lemulge12  10924  ltmuldiv2  10935  ltdivmul2  10938  lt2mul2div  10939  ledivmul2  10940  lemuldiv2  10942  supmul  11033  times2  11184  modcyc  12745  modcyc2  12746  modmulmodr  12776  subsq  13012  cjmulrcl  13928  imval2  13935  abscj  14063  sqabsadd  14066  sqabssub  14067  sqreulem  14143  iseraltlem2  14457  iseraltlem3  14458  climcndslem2  14626  prodfmul  14666  prodmolem3  14707  bpoly3  14833  efcllem  14852  efexp  14875  sinmul  14946  demoivreALT  14975  dvdsmul1  15050  odd2np1lem  15111  odd2np1  15112  opeo  15136  omeo  15137  modgcd  15300  bezoutlem1  15303  dvdsgcd  15308  gcdmultiple  15316  coprmdvds  15413  coprmdvdsOLD  15414  coprmdvds2  15415  qredeq  15418  eulerthlem2  15534  modprm0  15557  modprmn0modprm0  15559  coprimeprodsq2  15561  prmreclem6  15672  odmod  18011  cncrng  19815  cnsrng  19828  pcoass  22870  clmvscom  22936  dvlipcn  23802  plydivlem4  24096  quotcan  24109  aaliou3lem3  24144  ef2kpi  24275  sinperlem  24277  sinmpi  24284  cosmpi  24285  sinppi  24286  cosppi  24287  sineq0  24318  tanregt0  24330  logneg  24379  lognegb  24381  logimul  24405  tanarg  24410  logtayl  24451  cxpsqrtlem  24493  cubic2  24620  quart1  24628  log2cnv  24716  basellem1  24852  basellem3  24854  basellem5  24856  basellem8  24859  mumul  24952  chtublem  24981  perfectlem1  24999  perfectlem2  25000  perfect  25001  dchrabl  25024  bposlem6  25059  bposlem9  25062  lgsdir2lem4  25098  lgsdir2  25100  lgsdir  25102  lgsdi  25104  lgsquadlem2  25151  lgsquad2  25156  rpvmasum2  25246  mulog2sumlem1  25268  pntibndlem2  25325  pntibndlem3  25326  pntlemf  25339  nvscom  27612  ipasslem11  27823  ipblnfi  27839  hvmulcom  28028  h1de2bi  28541  homul12  28792  riesz3i  29049  riesz1  29052  kbass4  29106  sin2h  33529  heiborlem6  33745  rmym1  37817  expgrowthi  38849  expgrowth  38851  stoweidlem10  40545  perfectALTVlem1  41955  perfectALTVlem2  41956  perfectALTV  41957  tgoldbachlt  42029  tgoldbachltOLD  42035  2zrngnmlid2  42276
  Copyright terms: Public domain W3C validator