Theorem mulcom 10472

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522   ∈ wcel 2080  (class class class)co 7019  ℂcc 10384   · cmul 10391

This theorem was proved from axioms:  ax-mulcom 10450

This theorem is referenced by:  adddir  10481  mulid2  10489  mulcomi  10498  mulcomd  10511  mul12  10654  mul32  10655  mul31  10656  mul4r  10658  mul01  10668  muladd  10922  subdir  10924  mulneg2  10927  recextlem1  11120  mulcan2g  11144  divmul3  11153  div23  11167  div13  11169  div12  11170  divmulasscom  11172  divcan4  11175  divmul13  11193  divmul24  11194  divcan7  11199  div2neg  11213  prodgt02  11338  ltmul2  11341  lemul2  11343  lemul2a  11345  ltmulgt12  11351  lemulge12  11353  ltmuldiv2  11364  ltdivmul2  11367  lt2mul2div  11368  ledivmul2  11369  lemuldiv2  11371  supmul  11463  times2  11624  modcyc  13124  modcyc2  13125  modmulmodr  13155  subsq  13422  cjmulrcl  14337  imval2  14344  abscj  14473  sqabsadd  14476  sqabssub  14477  sqreulem  14553  iseraltlem2  14873  iseraltlem3  14874  climcndslem2  15038  prodfmul  15079  prodmolem3  15120  bpoly3  15245  efcllem  15264  efexp  15287  sinmul  15358  demoivreALT  15387  dvdsmul1  15464  odd2np1lem  15522  odd2np1  15523  opeo  15547  omeo  15548  modgcd  15713  bezoutlem1  15716  dvdsgcd  15721  gcdmultiple  15729  coprmdvds  15826  coprmdvds2  15827  qredeq  15830  eulerthlem2  15948  modprm0  15971  modprmn0modprm0  15973  coprimeprodsq2  15975  prmreclem6  16086  odmod  18405  cncrng  20248  cnsrng  20261  pcoass  23311  clmvscom  23377  dvlipcn  24274  plydivlem4  24568  quotcan  24581  aaliou3lem3  24616  ef2kpi  24747  sinperlem  24749  sinmpi  24756  cosmpi  24757  sinppi  24758  cosppi  24759  sineq0  24792  tanregt0  24804  logneg  24852  lognegb  24854  logimul  24878  tanarg  24883  logtayl  24924  cxpsqrtlem  24966  cxpcom  25001  cubic2  25107  quart1  25115  log2cnv  25204  basellem1  25340  basellem3  25342  basellem5  25344  basellem8  25347  mumul  25440  chtublem  25469  perfectlem1  25487  perfectlem2  25488  perfect  25489  dchrabl  25512  bposlem6  25547  bposlem9  25550  lgsdir2lem4  25586  lgsdir2  25588  lgsquadlem2  25639  lgsquad2  25644  rpvmasum2  25770  mulog2sumlem1  25792  pntibndlem2  25849  pntibndlem3  25850  pntlemf  25863  nvscom  28089  ipasslem11  28300  ipblnfi  28315  hvmulcom  28503  h1de2bi  29014  homul12  29265  riesz3i  29522  riesz1  29525  kbass4  29579  sin2h  34426  heiborlem6  34639  rmym1  39030  expgrowthi  40216  expgrowth  40218  stoweidlem10  41851  perfectALTVlem1  43382  perfectALTVlem2  43383  perfectALTV  43384  tgoldbachlt  43477  2zrngnmlid2  43714