Theorem mulcom 9901

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   · cmul 9820

This theorem was proved from axioms:  ax-mulcom 9879

This theorem is referenced by:  adddir  9910  mulid2  9917  mulcomi  9925  mulcomd  9940  mul12  10081  mul32  10082  mul31  10083  mul01  10094  muladd  10341  subdir  10343  mulneg2  10346  recextlem1  10536  mulcan2g  10560  divmul3  10569  div23  10583  div13  10585  div12  10586  divmulasscom  10588  divcan4  10591  divmul13  10607  divmul24  10608  divcan7  10613  div2neg  10627  prodgt02  10748  prodge02  10750  ltmul2  10753  lemul2  10755  lemul2a  10757  ltmulgt12  10763  lemulge12  10765  ltmuldiv2  10776  ltdivmul2  10779  lt2mul2div  10780  ledivmul2  10781  lemuldiv2  10783  supmul  10872  times2  11023  modcyc  12567  modcyc2  12568  modmulmodr  12598  subsq  12834  cjmulrcl  13732  imval2  13739  abscj  13867  sqabsadd  13870  sqabssub  13871  sqreulem  13947  iseraltlem2  14261  iseraltlem3  14262  climcndslem2  14421  prodfmul  14461  prodmolem3  14502  bpoly3  14628  efcllem  14647  efexp  14670  sinmul  14741  demoivreALT  14770  dvdsmul1  14841  odd2np1lem  14902  odd2np1  14903  opeo  14927  omeo  14928  modgcd  15091  bezoutlem1  15094  dvdsgcd  15099  gcdmultiple  15107  coprmdvds  15204  coprmdvdsOLD  15205  coprmdvds2  15206  qredeq  15209  eulerthlem2  15325  modprm0  15348  modprmn0modprm0  15350  coprimeprodsq2  15352  prmreclem6  15463  odmod  17788  cncrng  19586  cnsrng  19599  pcoass  22632  clmvscom  22698  dvlipcn  23561  plydivlem4  23855  quotcan  23868  aaliou3lem3  23903  ef2kpi  24034  sinperlem  24036  sinmpi  24043  cosmpi  24044  sinppi  24045  cosppi  24046  sineq0  24077  tanregt0  24089  logneg  24138  lognegb  24140  logimul  24164  tanarg  24169  logtayl  24206  cxpsqrtlem  24248  cubic2  24375  quart1  24383  log2cnv  24471  basellem1  24607  basellem3  24609  basellem5  24611  basellem8  24614  mumul  24707  chtublem  24736  perfectlem1  24754  perfectlem2  24755  perfect  24756  dchrabl  24779  bposlem6  24814  bposlem9  24817  lgsdir2lem4  24853  lgsdir2  24855  lgsdir  24857  lgsdi  24859  lgsquadlem2  24906  lgsquad2  24911  rpvmasum2  25001  mulog2sumlem1  25023  pntibndlem2  25080  pntibndlem3  25081  pntlemf  25094  nvscom  26868  ipasslem11  27079  ipblnfi  27095  hvmulcom  27284  h1de2bi  27797  homul12  28048  riesz3i  28305  riesz1  28308  kbass4  28362  sin2h  32569  heiborlem6  32785  rmym1  36518  expgrowthi  37554  expgrowth  37556  stoweidlem10  38903  perfectALTVlem1  40164  perfectALTVlem2  40165  perfectALTV  40166  tgoldbachlt  40230  tgoldbachltOLD  40237  2zrngnmlid2  41741