Theorem mulcom 10625

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  (class class class)co 7158  ℂcc 10537   · cmul 10544

This theorem was proved from axioms:  ax-mulcom 10603

This theorem is referenced by:  adddir  10634  mulid2  10642  mulcomi  10651  mulcomd  10664  mul12  10807  mul32  10808  mul31  10809  mul4r  10811  mul01  10821  muladd  11074  subdir  11076  mulneg2  11079  recextlem1  11272  mulcan2g  11296  divmul3  11305  div23  11319  div13  11321  div12  11322  divmulasscom  11324  divcan4  11327  divmul13  11345  divmul24  11346  divcan7  11351  div2neg  11365  prodgt02  11490  ltmul2  11493  lemul2  11495  lemul2a  11497  ltmulgt12  11503  lemulge12  11505  ltmuldiv2  11516  ltdivmul2  11519  lt2mul2div  11520  ledivmul2  11521  lemuldiv2  11523  supmul  11615  times2  11777  modcyc  13277  modcyc2  13278  modmulmodr  13308  subsq  13575  cjmulrcl  14505  imval2  14512  abscj  14641  sqabsadd  14644  sqabssub  14645  sqreulem  14721  iseraltlem2  15041  iseraltlem3  15042  climcndslem2  15207  prodfmul  15248  prodmolem3  15289  bpoly3  15414  efcllem  15433  efexp  15456  sinmul  15527  demoivreALT  15556  dvdsmul1  15633  odd2np1lem  15691  odd2np1  15692  opeo  15716  omeo  15717  modgcd  15882  bezoutlem1  15889  dvdsgcd  15894  gcdmultipleOLD  15902  coprmdvds  15999  coprmdvds2  16000  qredeq  16003  eulerthlem2  16121  modprm0  16144  modprmn0modprm0  16146  coprimeprodsq2  16148  prmreclem6  16259  odmod  18676  cncrng  20568  cnsrng  20581  pcoass  23630  clmvscom  23696  dvlipcn  24593  plydivlem4  24887  quotcan  24900  aaliou3lem3  24935  ef2kpi  25066  sinperlem  25068  sinmpi  25075  cosmpi  25076  sinppi  25077  cosppi  25078  sineq0  25111  tanregt0  25125  logneg  25173  lognegb  25175  logimul  25199  tanarg  25204  logtayl  25245  cxpsqrtlem  25287  cxpcom  25322  cubic2  25428  quart1  25436  log2cnv  25524  basellem1  25660  basellem3  25662  basellem5  25664  basellem8  25667  mumul  25760  chtublem  25789  perfectlem1  25807  perfectlem2  25808  perfect  25809  dchrabl  25832  bposlem6  25867  bposlem9  25870  lgsdir2lem4  25906  lgsdir2  25908  lgsquadlem2  25959  lgsquad2  25964  rpvmasum2  26090  mulog2sumlem1  26112  pntibndlem2  26169  pntibndlem3  26170  pntlemf  26183  nvscom  28408  ipasslem11  28619  ipblnfi  28634  hvmulcom  28822  h1de2bi  29333  homul12  29584  riesz3i  29841  riesz1  29844  kbass4  29898  sin2h  34884  heiborlem6  35096  rmym1  39539  expgrowthi  40672  expgrowth  40674  stoweidlem10  42302  perfectALTVlem1  43893  perfectALTVlem2  43894  perfectALTV  43895  tgoldbachlt  43988  2zrngnmlid2  44229