Theorem mulcom 11214

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

Assertion

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

Proof of Theorem mulcom

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

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

This proof depends on axioms:  ax-mulcom 11192

This theorem is used by:  adddir  11225  mullid  11235  mulcomi  11245  mulcomd  11258  mul12  11403  mul32  11404  mul31  11405  mul4r  11407  mul01  11417  muladd  11674  subdir  11676  mulneg2  11679  recextlem1  11872  mulcan2g  11896  divmul3  11905  div23  11919  div13  11921  div12  11922  divmulasscom  11924  divcan4  11927  divmul13  11946  divmul24  11947  divcan7  11952  div2neg  11966  prodgt02  12091  ltmul2  12094  lemul2  12096  lemul2a  12098  ltmulgt12  12103  lemulge12  12106  ltmuldiv2  12117  ltdivmul2  12120  lt2mul2div  12121  ledivmul2  12122  lemuldiv2  12124  supmul  12215  times2  12405  modcyc  13971  modcyc2  13972  modmulmodr  14005  subsq  14278  cjmulrcl  15235  imval2  15242  abscj  15370  sqabsadd  15373  sqabssub  15374  sqreulem  15451  iseraltlem2  15774  iseraltlem3  15775  climcndslem2  15943  prodfmul  15983  prodmolem3  16026  bpoly3  16150  efcllem  16169  efexp  16195  sinmul  16266  demoivreALT  16295  dvdsmul1  16373  odd2np1lem  16436  odd2np1  16437  opeo  16461  omeo  16462  modgcd  16628  bezoutlem1  16635  dvdsgcd  16640  coprmdvds  16749  coprmdvds2  16750  qredeq  16753  eulerthlem2  16879  modprm0  16903  modprmn0modprm0  16905  coprimeprodsq2  16907  prmreclem6  17019  odmod  19679  cncrng  21612  cnsrng  21625  pcoass  25258  clmvscom  25324  dvlipcn  26228  plydivlem4  26533  quotcan  26548  aaliou3lem3  26587  ef2kpi  26723  sinperlem  26725  sinmpi  26732  cosmpi  26733  sinppi  26734  cosppi  26735  sineq0  26769  tanregt0  26784  logneg  26833  lognegb  26835  logimul  26859  tanarg  26864  logtayl  26905  cxpsqrtlem  26947  cxpcom  26984  cubic2  27093  quart1  27101  log2cnv  27189  basellem1  27325  basellem3  27327  basellem5  27329  mumul  27425  chtublem  27455  perfectlem1  27473  perfectlem2  27474  perfect  27475  dchrabl  27498  bposlem6  27533  bposlem9  27536  lgsdir2lem4  27572  lgsdir2  27574  lgsquadlem2  27625  lgsquad2  27630  rpvmasum2  27756  mulog2sumlem1  27778  pntibndlem2  27835  pntibndlem3  27836  pntlemf  27849  nvscom  31118  ipasslem11  31329  ipblnfi  31344  hvmulcom  31532  h1de2bi  32043  homul12  32294  riesz3i  32551  riesz1  32554  kbass4  32608  sin2h  38372  heiborlem6  38574  rmym1  43784  expgrowthi  45165  expgrowth  45167  stoweidlem10  46846  perfectALTVlem1  48645  perfectALTVlem2  48646  perfectALTV  48647  tgoldbachlt  48740  2zrngnmlid2  49180