Theorem mulcom 11313

Description: Alias for ax-mulcom 11291, for naming consistency with mulcomi 11344. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
mulcom	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

Proof of Theorem mulcom

Step	Hyp	Ref	Expression
1		ax-mulcom 11291	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225   · cmul 11232

This proof depends on axioms:  ax-mulcom 11291

This theorem is used by:  adddir  11324  mullid  11334  mulcomi  11344  mulcomd  11357  mul12  11502  mul32  11503  mul31  11504  mul4r  11506  mul01  11516  muladd  11775  subdir  11777  mulneg2  11780  recextlem1  11973  mulcan2g  11997  divmul3  12006  div23  12020  div13  12022  div12  12023  divmulasscom  12025  divcan4  12028  divmul13  12047  divmul24  12048  divcan7  12053  div2neg  12067  prodgt02  12192  ltmul2  12195  lemul2  12197  lemul2a  12199  ltmulgt12  12204  lemulge12  12207  ltmuldiv2  12218  ltdivmul2  12221  lt2mul2div  12222  ledivmul2  12223  lemuldiv2  12225  supmul  12316  times2  12506  modcyc  14073  modcyc2  14074  modmulmodr  14107  subsq  14381  cjmulrcl  15340  imval2  15347  abscj  15475  sqabsadd  15478  sqabssub  15479  sqreulem  15556  iseraltlem2  15879  iseraltlem3  15880  climcndslem2  16048  prodfmul  16088  prodmolem3  16129  bpoly3  16253  efcllem  16272  efexp  16298  sinmul  16369  demoivreALT  16398  dvdsmul1  16476  odd2np1lem  16539  odd2np1  16540  opeo  16564  omeo  16565  modgcd  16734  bezoutlem1  16741  dvdsgcd  16746  coprmdvds  16857  coprmdvds2  16858  qredeq  16861  eulerthlem2  16988  modprm0  17012  modprmn0modprm0  17014  coprimeprodsq2  17016  prmreclem6  17128  odmod  19790  cncrng  21729  cnsrng  21742  pcoass  25375  clmvscom  25441  dvlipcn  26344  plydivlem4  26647  quotcan  26662  aaliou3lem3  26701  ef2kpi  26837  sinperlem  26839  sinmpi  26846  cosmpi  26847  sinppi  26848  cosppi  26849  sineq0  26882  tanregt0  26897  logneg  26946  lognegb  26948  logimul  26972  tanarg  26977  logtayl  27018  cxpsqrtlem  27060  cxpcom  27097  cubic2  27206  quart1  27214  log2cnv  27302  basellem1  27438  basellem3  27440  basellem5  27442  chtublem  27568  perfectlem1  27586  perfectlem2  27587  perfect  27588  dchrabl  27611  bposlem6  27646  bposlem9  27649  lgsdir2lem4  27685  lgsdir2  27687  lgsquadlem2  27738  lgsquad2  27743  rpvmasum2  27869  mulog2sumlem1  27891  pntibndlem2  27948  pntibndlem3  27949  pntlemf  27962  nvscom  31261  ipasslem11  31472  ipblnfi  31487  hvmulcom  31675  h1de2bi  32186  homul12  32437  riesz3i  32694  riesz1  32697  kbass4  32751  sin2h  38725  heiborlem6  38942  rmym1  44135  expgrowthi  45509  expgrowth  45511  stoweidlem10  47225  perfectALTVlem1  49024  perfectALTVlem2  49025  perfectALTV  49026  tgoldbachlt  49119  2zrngnmlid2  49559