Theorem mulcom 10623

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   · cmul 10542

This theorem was proved from axioms:  ax-mulcom 10601

This theorem is referenced by:  adddir  10632  mulid2  10640  mulcomi  10649  mulcomd  10662  mul12  10805  mul32  10806  mul31  10807  mul4r  10809  mul01  10819  muladd  11072  subdir  11074  mulneg2  11077  recextlem1  11270  mulcan2g  11294  divmul3  11303  div23  11317  div13  11319  div12  11320  divmulasscom  11322  divcan4  11325  divmul13  11343  divmul24  11344  divcan7  11349  div2neg  11363  prodgt02  11488  ltmul2  11491  lemul2  11493  lemul2a  11495  ltmulgt12  11501  lemulge12  11503  ltmuldiv2  11514  ltdivmul2  11517  lt2mul2div  11518  ledivmul2  11519  lemuldiv2  11521  supmul  11613  times2  11775  modcyc  13275  modcyc2  13276  modmulmodr  13306  subsq  13573  cjmulrcl  14503  imval2  14510  abscj  14639  sqabsadd  14642  sqabssub  14643  sqreulem  14719  iseraltlem2  15039  iseraltlem3  15040  climcndslem2  15205  prodfmul  15246  prodmolem3  15287  bpoly3  15412  efcllem  15431  efexp  15454  sinmul  15525  demoivreALT  15554  dvdsmul1  15631  odd2np1lem  15689  odd2np1  15690  opeo  15714  omeo  15715  modgcd  15880  bezoutlem1  15887  dvdsgcd  15892  gcdmultipleOLD  15900  coprmdvds  15997  coprmdvds2  15998  qredeq  16001  eulerthlem2  16119  modprm0  16142  modprmn0modprm0  16144  coprimeprodsq2  16146  prmreclem6  16257  odmod  18674  cncrng  20566  cnsrng  20579  pcoass  23628  clmvscom  23694  dvlipcn  24591  plydivlem4  24885  quotcan  24898  aaliou3lem3  24933  ef2kpi  25064  sinperlem  25066  sinmpi  25073  cosmpi  25074  sinppi  25075  cosppi  25076  sineq0  25109  tanregt0  25123  logneg  25171  lognegb  25173  logimul  25197  tanarg  25202  logtayl  25243  cxpsqrtlem  25285  cxpcom  25320  cubic2  25426  quart1  25434  log2cnv  25522  basellem1  25658  basellem3  25660  basellem5  25662  basellem8  25665  mumul  25758  chtublem  25787  perfectlem1  25805  perfectlem2  25806  perfect  25807  dchrabl  25830  bposlem6  25865  bposlem9  25868  lgsdir2lem4  25904  lgsdir2  25906  lgsquadlem2  25957  lgsquad2  25962  rpvmasum2  26088  mulog2sumlem1  26110  pntibndlem2  26167  pntibndlem3  26168  pntlemf  26181  nvscom  28406  ipasslem11  28617  ipblnfi  28632  hvmulcom  28820  h1de2bi  29331  homul12  29582  riesz3i  29839  riesz1  29842  kbass4  29896  sin2h  34897  heiborlem6  35109  rmym1  39552  expgrowthi  40685  expgrowth  40687  stoweidlem10  42315  perfectALTVlem1  43906  perfectALTVlem2  43907  perfectALTV  43908  tgoldbachlt  44001  2zrngnmlid2  44242