Theorem mulcom 9966

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  (class class class)co 6604  ℂcc 9878   · cmul 9885

This theorem was proved from axioms:  ax-mulcom 9944

This theorem is referenced by:  adddir  9975  mulid2  9982  mulcomi  9990  mulcomd  10005  mul12  10146  mul32  10147  mul31  10148  mul01  10159  muladd  10406  subdir  10408  mulneg2  10411  recextlem1  10601  mulcan2g  10625  divmul3  10634  div23  10648  div13  10650  div12  10651  divmulasscom  10653  divcan4  10656  divmul13  10672  divmul24  10673  divcan7  10678  div2neg  10692  prodgt02  10813  prodge02  10815  ltmul2  10818  lemul2  10820  lemul2a  10822  ltmulgt12  10828  lemulge12  10830  ltmuldiv2  10841  ltdivmul2  10844  lt2mul2div  10845  ledivmul2  10846  lemuldiv2  10848  supmul  10939  times2  11090  modcyc  12645  modcyc2  12646  modmulmodr  12676  subsq  12912  cjmulrcl  13818  imval2  13825  abscj  13953  sqabsadd  13956  sqabssub  13957  sqreulem  14033  iseraltlem2  14347  iseraltlem3  14348  climcndslem2  14507  prodfmul  14547  prodmolem3  14588  bpoly3  14714  efcllem  14733  efexp  14756  sinmul  14827  demoivreALT  14856  dvdsmul1  14927  odd2np1lem  14988  odd2np1  14989  opeo  15013  omeo  15014  modgcd  15177  bezoutlem1  15180  dvdsgcd  15185  gcdmultiple  15193  coprmdvds  15290  coprmdvdsOLD  15291  coprmdvds2  15292  qredeq  15295  eulerthlem2  15411  modprm0  15434  modprmn0modprm0  15436  coprimeprodsq2  15438  prmreclem6  15549  odmod  17886  cncrng  19686  cnsrng  19699  pcoass  22732  clmvscom  22798  dvlipcn  23661  plydivlem4  23955  quotcan  23968  aaliou3lem3  24003  ef2kpi  24134  sinperlem  24136  sinmpi  24143  cosmpi  24144  sinppi  24145  cosppi  24146  sineq0  24177  tanregt0  24189  logneg  24238  lognegb  24240  logimul  24264  tanarg  24269  logtayl  24306  cxpsqrtlem  24348  cubic2  24475  quart1  24483  log2cnv  24571  basellem1  24707  basellem3  24709  basellem5  24711  basellem8  24714  mumul  24807  chtublem  24836  perfectlem1  24854  perfectlem2  24855  perfect  24856  dchrabl  24879  bposlem6  24914  bposlem9  24917  lgsdir2lem4  24953  lgsdir2  24955  lgsdir  24957  lgsdi  24959  lgsquadlem2  25006  lgsquad2  25011  rpvmasum2  25101  mulog2sumlem1  25123  pntibndlem2  25180  pntibndlem3  25181  pntlemf  25194  nvscom  27333  ipasslem11  27544  ipblnfi  27560  hvmulcom  27749  h1de2bi  28262  homul12  28513  riesz3i  28770  riesz1  28773  kbass4  28827  sin2h  33031  heiborlem6  33247  rmym1  36980  expgrowthi  38014  expgrowth  38016  stoweidlem10  39534  perfectALTVlem1  40925  perfectALTVlem2  40926  perfectALTV  40927  tgoldbachlt  40991  tgoldbachltOLD  40998  2zrngnmlid2  41239