Theorem mulcom 11270

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   · cmul 11189

This theorem was proved from axioms:  ax-mulcom 11248

This theorem is referenced by:  adddir  11281  mullid  11289  mulcomi  11298  mulcomd  11311  mul12  11455  mul32  11456  mul31  11457  mul4r  11459  mul01  11469  muladd  11722  subdir  11724  mulneg2  11727  recextlem1  11920  mulcan2g  11944  divmul3  11954  div23  11968  div13  11970  div12  11971  divmulasscom  11973  divcan4  11976  divmul13  11997  divmul24  11998  divcan7  12003  div2neg  12017  prodgt02  12142  ltmul2  12145  lemul2  12147  lemul2a  12149  ltmulgt12  12155  lemulge12  12158  ltmuldiv2  12169  ltdivmul2  12172  lt2mul2div  12173  ledivmul2  12174  lemuldiv2  12176  supmul  12267  times2  12430  modcyc  13957  modcyc2  13958  modmulmodr  13988  subsq  14259  cjmulrcl  15193  imval2  15200  abscj  15328  sqabsadd  15331  sqabssub  15332  sqreulem  15408  iseraltlem2  15731  iseraltlem3  15732  climcndslem2  15898  prodfmul  15938  prodmolem3  15981  bpoly3  16106  efcllem  16125  efexp  16149  sinmul  16220  demoivreALT  16249  dvdsmul1  16326  odd2np1lem  16388  odd2np1  16389  opeo  16413  omeo  16414  modgcd  16579  bezoutlem1  16586  dvdsgcd  16591  coprmdvds  16700  coprmdvds2  16701  qredeq  16704  eulerthlem2  16829  modprm0  16852  modprmn0modprm0  16854  coprimeprodsq2  16856  prmreclem6  16968  odmod  19588  cncrng  21424  cncrngOLD  21425  cnsrng  21441  pcoass  25076  clmvscom  25142  dvlipcn  26053  plydivlem4  26356  quotcan  26369  aaliou3lem3  26404  ef2kpi  26538  sinperlem  26540  sinmpi  26547  cosmpi  26548  sinppi  26549  cosppi  26550  sineq0  26584  tanregt0  26599  logneg  26648  lognegb  26650  logimul  26674  tanarg  26679  logtayl  26720  cxpsqrtlem  26762  cxpcom  26799  cubic2  26909  quart1  26917  log2cnv  27005  basellem1  27142  basellem3  27144  basellem5  27146  basellem8  27149  mumul  27242  chtublem  27273  perfectlem1  27291  perfectlem2  27292  perfect  27293  dchrabl  27316  bposlem6  27351  bposlem9  27354  lgsdir2lem4  27390  lgsdir2  27392  lgsquadlem2  27443  lgsquad2  27448  rpvmasum2  27574  mulog2sumlem1  27596  pntibndlem2  27653  pntibndlem3  27654  pntlemf  27667  nvscom  30661  ipasslem11  30872  ipblnfi  30887  hvmulcom  31075  h1de2bi  31586  homul12  31837  riesz3i  32094  riesz1  32097  kbass4  32151  sin2h  37570  heiborlem6  37776  rmym1  42892  expgrowthi  44302  expgrowth  44304  stoweidlem10  45931  perfectALTVlem1  47595  perfectALTVlem2  47596  perfectALTV  47597  tgoldbachlt  47690  2zrngnmlid2  47980