Theorem mulcom 11114

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   · cmul 11033

This theorem was proved from axioms:  ax-mulcom 11092

This theorem is referenced by:  adddir  11125  mullid  11133  mulcomi  11142  mulcomd  11155  mul12  11299  mul32  11300  mul31  11301  mul4r  11303  mul01  11313  muladd  11570  subdir  11572  mulneg2  11575  recextlem1  11768  mulcan2g  11792  divmul3  11802  div23  11816  div13  11818  div12  11819  divmulasscom  11821  divcan4  11824  divmul13  11845  divmul24  11846  divcan7  11851  div2neg  11865  prodgt02  11990  ltmul2  11993  lemul2  11995  lemul2a  11997  ltmulgt12  12003  lemulge12  12006  ltmuldiv2  12017  ltdivmul2  12020  lt2mul2div  12021  ledivmul2  12022  lemuldiv2  12024  supmul  12115  times2  12278  modcyc  13828  modcyc2  13829  modmulmodr  13862  subsq  14135  cjmulrcl  15069  imval2  15076  abscj  15204  sqabsadd  15207  sqabssub  15208  sqreulem  15285  iseraltlem2  15608  iseraltlem3  15609  climcndslem2  15775  prodfmul  15815  prodmolem3  15858  bpoly3  15983  efcllem  16002  efexp  16028  sinmul  16099  demoivreALT  16128  dvdsmul1  16206  odd2np1lem  16269  odd2np1  16270  opeo  16294  omeo  16295  modgcd  16461  bezoutlem1  16468  dvdsgcd  16473  coprmdvds  16582  coprmdvds2  16583  qredeq  16586  eulerthlem2  16711  modprm0  16735  modprmn0modprm0  16737  coprimeprodsq2  16739  prmreclem6  16851  odmod  19443  cncrng  21313  cncrngOLD  21314  cnsrng  21330  pcoass  24940  clmvscom  25006  dvlipcn  25915  plydivlem4  26220  quotcan  26233  aaliou3lem3  26268  ef2kpi  26403  sinperlem  26405  sinmpi  26412  cosmpi  26413  sinppi  26414  cosppi  26415  sineq0  26449  tanregt0  26464  logneg  26513  lognegb  26515  logimul  26539  tanarg  26544  logtayl  26585  cxpsqrtlem  26627  cxpcom  26664  cubic2  26774  quart1  26782  log2cnv  26870  basellem1  27007  basellem3  27009  basellem5  27011  basellem8  27014  mumul  27107  chtublem  27138  perfectlem1  27156  perfectlem2  27157  perfect  27158  dchrabl  27181  bposlem6  27216  bposlem9  27219  lgsdir2lem4  27255  lgsdir2  27257  lgsquadlem2  27308  lgsquad2  27313  rpvmasum2  27439  mulog2sumlem1  27461  pntibndlem2  27518  pntibndlem3  27519  pntlemf  27532  nvscom  30591  ipasslem11  30802  ipblnfi  30817  hvmulcom  31005  h1de2bi  31516  homul12  31767  riesz3i  32024  riesz1  32027  kbass4  32081  sin2h  37589  heiborlem6  37795  rmym1  42908  expgrowthi  44306  expgrowth  44308  stoweidlem10  45992  perfectALTVlem1  47706  perfectALTVlem2  47707  perfectALTV  47708  tgoldbachlt  47801  2zrngnmlid2  48242