Theorem mulcom 11187

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  (class class class)co 7412  ℂcc 11099   · cmul 11106

This theorem was proved from axioms:  ax-mulcom 11165

This theorem is referenced by:  adddir  11198  mullid  11208  mulcomi  11218  mulcomd  11231  mul12  11376  mul32  11377  mul31  11378  mul4r  11380  mul01  11390  muladd  11647  subdir  11649  mulneg2  11652  recextlem1  11845  mulcan2g  11869  divmul3  11878  div23  11892  div13  11894  div12  11895  divmulasscom  11897  divcan4  11900  divmul13  11919  divmul24  11920  divcan7  11925  div2neg  11939  prodgt02  12064  ltmul2  12067  lemul2  12069  lemul2a  12071  ltmulgt12  12076  lemulge12  12079  ltmuldiv2  12090  ltdivmul2  12093  lt2mul2div  12094  ledivmul2  12095  lemuldiv2  12097  supmul  12188  times2  12378  modcyc  13941  modcyc2  13942  modmulmodr  13975  subsq  14248  cjmulrcl  15197  imval2  15204  abscj  15332  sqabsadd  15335  sqabssub  15336  sqreulem  15413  iseraltlem2  15736  iseraltlem3  15737  climcndslem2  15906  prodfmul  15946  prodmolem3  15989  bpoly3  16113  efcllem  16132  efexp  16158  sinmul  16229  demoivreALT  16258  dvdsmul1  16336  odd2np1lem  16399  odd2np1  16400  opeo  16424  omeo  16425  modgcd  16591  bezoutlem1  16598  dvdsgcd  16603  coprmdvds  16712  coprmdvds2  16713  qredeq  16716  eulerthlem2  16842  modprm0  16866  modprmn0modprm0  16868  coprimeprodsq2  16870  prmreclem6  16982  odmod  19617  cncrng  21524  cnsrng  21537  pcoass  25164  clmvscom  25230  dvlipcn  26134  plydivlem4  26438  quotcan  26451  aaliou3lem3  26486  ef2kpi  26621  sinperlem  26623  sinmpi  26630  cosmpi  26631  sinppi  26632  cosppi  26633  sineq0  26667  tanregt0  26682  logneg  26731  lognegb  26733  logimul  26757  tanarg  26762  logtayl  26803  cxpsqrtlem  26845  cxpcom  26882  cubic2  26991  quart1  26999  log2cnv  27087  basellem1  27223  basellem3  27225  basellem5  27227  basellem8  27230  mumul  27323  chtublem  27353  perfectlem1  27371  perfectlem2  27372  perfect  27373  dchrabl  27396  bposlem6  27431  bposlem9  27434  lgsdir2lem4  27470  lgsdir2  27472  lgsquadlem2  27523  lgsquad2  27528  rpvmasum2  27654  mulog2sumlem1  27676  pntibndlem2  27733  pntibndlem3  27734  pntlemf  27747  nvscom  30959  ipasslem11  31170  ipblnfi  31185  hvmulcom  31373  h1de2bi  31884  homul12  32135  riesz3i  32392  riesz1  32395  kbass4  32449  sin2h  38239  heiborlem6  38445  rmym1  43642  expgrowthi  45023  expgrowth  45025  stoweidlem10  46704  perfectALTVlem1  48463  perfectALTVlem2  48464  perfectALTV  48465  tgoldbachlt  48558  2zrngnmlid2  48999