Theorem mulcom 11241

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   · cmul 11160

This theorem was proved from axioms:  ax-mulcom 11219

This theorem is referenced by:  adddir  11252  mullid  11260  mulcomi  11269  mulcomd  11282  mul12  11426  mul32  11427  mul31  11428  mul4r  11430  mul01  11440  muladd  11695  subdir  11697  mulneg2  11700  recextlem1  11893  mulcan2g  11917  divmul3  11927  div23  11941  div13  11943  div12  11944  divmulasscom  11946  divcan4  11949  divmul13  11970  divmul24  11971  divcan7  11976  div2neg  11990  prodgt02  12115  ltmul2  12118  lemul2  12120  lemul2a  12122  ltmulgt12  12128  lemulge12  12131  ltmuldiv2  12142  ltdivmul2  12145  lt2mul2div  12146  ledivmul2  12147  lemuldiv2  12149  supmul  12240  times2  12403  modcyc  13946  modcyc2  13947  modmulmodr  13978  subsq  14249  cjmulrcl  15183  imval2  15190  abscj  15318  sqabsadd  15321  sqabssub  15322  sqreulem  15398  iseraltlem2  15719  iseraltlem3  15720  climcndslem2  15886  prodfmul  15926  prodmolem3  15969  bpoly3  16094  efcllem  16113  efexp  16137  sinmul  16208  demoivreALT  16237  dvdsmul1  16315  odd2np1lem  16377  odd2np1  16378  opeo  16402  omeo  16403  modgcd  16569  bezoutlem1  16576  dvdsgcd  16581  coprmdvds  16690  coprmdvds2  16691  qredeq  16694  eulerthlem2  16819  modprm0  16843  modprmn0modprm0  16845  coprimeprodsq2  16847  prmreclem6  16959  odmod  19564  cncrng  21401  cncrngOLD  21402  cnsrng  21418  pcoass  25057  clmvscom  25123  dvlipcn  26033  plydivlem4  26338  quotcan  26351  aaliou3lem3  26386  ef2kpi  26520  sinperlem  26522  sinmpi  26529  cosmpi  26530  sinppi  26531  cosppi  26532  sineq0  26566  tanregt0  26581  logneg  26630  lognegb  26632  logimul  26656  tanarg  26661  logtayl  26702  cxpsqrtlem  26744  cxpcom  26781  cubic2  26891  quart1  26899  log2cnv  26987  basellem1  27124  basellem3  27126  basellem5  27128  basellem8  27131  mumul  27224  chtublem  27255  perfectlem1  27273  perfectlem2  27274  perfect  27275  dchrabl  27298  bposlem6  27333  bposlem9  27336  lgsdir2lem4  27372  lgsdir2  27374  lgsquadlem2  27425  lgsquad2  27430  rpvmasum2  27556  mulog2sumlem1  27578  pntibndlem2  27635  pntibndlem3  27636  pntlemf  27649  nvscom  30648  ipasslem11  30859  ipblnfi  30874  hvmulcom  31062  h1de2bi  31573  homul12  31824  riesz3i  32081  riesz1  32084  kbass4  32138  sin2h  37617  heiborlem6  37823  rmym1  42947  expgrowthi  44352  expgrowth  44354  stoweidlem10  46025  perfectALTVlem1  47708  perfectALTVlem2  47709  perfectALTV  47710  tgoldbachlt  47803  2zrngnmlid2  48173