Theorem mulcom 11267

Description: Alias for ax-mulcom 11245, 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 11245	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  (class class class)co 7412  ℂcc 11179   · cmul 11186

This proof depends on axioms:  ax-mulcom 11245

This theorem is used by:  adddir  11278  mullid  11288  mulcomi  11298  mulcomd  11311  mul12  11456  mul32  11457  mul31  11458  mul4r  11460  mul01  11470  muladd  11729  subdir  11731  mulneg2  11734  recextlem1  11927  mulcan2g  11951  divmul3  11960  div23  11974  div13  11976  div12  11977  divmulasscom  11979  divcan4  11982  divmul13  12001  divmul24  12002  divcan7  12007  div2neg  12021  prodgt02  12146  ltmul2  12149  lemul2  12151  lemul2a  12153  ltmulgt12  12158  lemulge12  12161  ltmuldiv2  12172  ltdivmul2  12175  lt2mul2div  12176  ledivmul2  12177  lemuldiv2  12179  supmul  12270  times2  12460  modcyc  14026  modcyc2  14027  modmulmodr  14060  subsq  14334  cjmulrcl  15291  imval2  15298  abscj  15426  sqabsadd  15429  sqabssub  15430  sqreulem  15507  iseraltlem2  15830  iseraltlem3  15831  climcndslem2  15999  prodfmul  16039  prodmolem3  16080  bpoly3  16204  efcllem  16223  efexp  16249  sinmul  16320  demoivreALT  16349  dvdsmul1  16427  odd2np1lem  16490  odd2np1  16491  opeo  16515  omeo  16516  modgcd  16685  bezoutlem1  16692  dvdsgcd  16697  coprmdvds  16808  coprmdvds2  16809  qredeq  16812  eulerthlem2  16939  modprm0  16963  modprmn0modprm0  16965  coprimeprodsq2  16967  prmreclem6  17079  odmod  19740  cncrng  21679  cnsrng  21692  pcoass  25325  clmvscom  25391  dvlipcn  26294  plydivlem4  26599  quotcan  26614  aaliou3lem3  26653  ef2kpi  26789  sinperlem  26791  sinmpi  26798  cosmpi  26799  sinppi  26800  cosppi  26801  sineq0  26834  tanregt0  26849  logneg  26898  lognegb  26900  logimul  26924  tanarg  26929  logtayl  26970  cxpsqrtlem  27012  cxpcom  27049  cubic2  27158  quart1  27166  log2cnv  27254  basellem1  27390  basellem3  27392  basellem5  27394  mumul  27490  chtublem  27520  perfectlem1  27538  perfectlem2  27539  perfect  27540  dchrabl  27563  bposlem6  27598  bposlem9  27601  lgsdir2lem4  27637  lgsdir2  27639  lgsquadlem2  27690  lgsquad2  27695  rpvmasum2  27821  mulog2sumlem1  27843  pntibndlem2  27900  pntibndlem3  27901  pntlemf  27914  nvscom  31213  ipasslem11  31424  ipblnfi  31439  hvmulcom  31627  h1de2bi  32138  homul12  32389  riesz3i  32646  riesz1  32649  kbass4  32703  sin2h  38501  heiborlem6  38718  rmym1  43895  expgrowthi  45276  expgrowth  45278  stoweidlem10  46964  perfectALTVlem1  48763  perfectALTVlem2  48764  perfectALTV  48765  tgoldbachlt  48858  2zrngnmlid2  49298