Theorem mulcom 10966

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  (class class class)co 7284  ℂcc 10878   · cmul 10885

This theorem was proved from axioms:  ax-mulcom 10944

This theorem is referenced by:  adddir  10975  mulid2  10983  mulcomi  10992  mulcomd  11005  mul12  11149  mul32  11150  mul31  11151  mul4r  11153  mul01  11163  muladd  11416  subdir  11418  mulneg2  11421  recextlem1  11614  mulcan2g  11638  divmul3  11647  div23  11661  div13  11663  div12  11664  divmulasscom  11666  divcan4  11669  divmul13  11687  divmul24  11688  divcan7  11693  div2neg  11707  prodgt02  11832  ltmul2  11835  lemul2  11837  lemul2a  11839  ltmulgt12  11845  lemulge12  11847  ltmuldiv2  11858  ltdivmul2  11861  lt2mul2div  11862  ledivmul2  11863  lemuldiv2  11865  supmul  11956  times2  12119  modcyc  13635  modcyc2  13636  modmulmodr  13666  subsq  13935  cjmulrcl  14864  imval2  14871  abscj  15000  sqabsadd  15003  sqabssub  15004  sqreulem  15080  iseraltlem2  15403  iseraltlem3  15404  climcndslem2  15571  prodfmul  15611  prodmolem3  15652  bpoly3  15777  efcllem  15796  efexp  15819  sinmul  15890  demoivreALT  15919  dvdsmul1  15996  odd2np1lem  16058  odd2np1  16059  opeo  16083  omeo  16084  modgcd  16249  bezoutlem1  16256  dvdsgcd  16261  gcdmultipleOLD  16269  coprmdvds  16367  coprmdvds2  16368  qredeq  16371  eulerthlem2  16492  modprm0  16515  modprmn0modprm0  16517  coprimeprodsq2  16519  prmreclem6  16631  odmod  19163  cncrng  20628  cnsrng  20641  pcoass  24196  clmvscom  24262  dvlipcn  25167  plydivlem4  25465  quotcan  25478  aaliou3lem3  25513  ef2kpi  25644  sinperlem  25646  sinmpi  25653  cosmpi  25654  sinppi  25655  cosppi  25656  sineq0  25689  tanregt0  25704  logneg  25752  lognegb  25754  logimul  25778  tanarg  25783  logtayl  25824  cxpsqrtlem  25866  cxpcom  25901  cubic2  26007  quart1  26015  log2cnv  26103  basellem1  26239  basellem3  26241  basellem5  26243  basellem8  26246  mumul  26339  chtublem  26368  perfectlem1  26386  perfectlem2  26387  perfect  26388  dchrabl  26411  bposlem6  26446  bposlem9  26449  lgsdir2lem4  26485  lgsdir2  26487  lgsquadlem2  26538  lgsquad2  26543  rpvmasum2  26669  mulog2sumlem1  26691  pntibndlem2  26748  pntibndlem3  26749  pntlemf  26762  nvscom  29000  ipasslem11  29211  ipblnfi  29226  hvmulcom  29414  h1de2bi  29925  homul12  30176  riesz3i  30433  riesz1  30436  kbass4  30490  sin2h  35776  heiborlem6  35983  rmym1  40764  expgrowthi  41958  expgrowth  41960  stoweidlem10  43558  perfectALTVlem1  45184  perfectALTVlem2  45185  perfectALTV  45186  tgoldbachlt  45279  2zrngnmlid2  45520