Theorem mulcom 10275

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1652   ∈ wcel 2155  (class class class)co 6842  ℂcc 10187   · cmul 10194

This theorem was proved from axioms:  ax-mulcom 10253

This theorem is referenced by:  adddir  10284  mulid2  10292  mulcomi  10302  mulcomd  10315  mul12  10456  mul32  10457  mul31  10458  mul01  10469  muladd  10716  subdir  10718  mulneg2  10721  recextlem1  10911  mulcan2g  10935  divmul3  10944  div23  10958  div13  10960  div12  10961  divmulasscom  10963  divcan4  10966  divmul13  10982  divmul24  10983  divcan7  10988  div2neg  11002  prodgt02  11123  prodge02OLD  11125  ltmul2  11128  lemul2  11130  lemul2a  11132  ltmulgt12  11138  lemulge12  11140  ltmuldiv2  11151  ltdivmul2  11154  lt2mul2div  11155  ledivmul2  11156  lemuldiv2  11158  supmul  11249  times2  11416  modcyc  12913  modcyc2  12914  modmulmodr  12944  subsq  13179  cjmulrcl  14169  imval2  14176  abscj  14304  sqabsadd  14307  sqabssub  14308  sqreulem  14384  iseraltlem2  14698  iseraltlem3  14699  climcndslem2  14866  prodfmul  14905  prodmolem3  14946  bpoly3  15071  efcllem  15090  efexp  15113  sinmul  15184  demoivreALT  15213  dvdsmul1  15288  odd2np1lem  15346  odd2np1  15347  opeo  15371  omeo  15372  modgcd  15534  bezoutlem1  15537  dvdsgcd  15542  gcdmultiple  15550  coprmdvds  15647  coprmdvds2  15648  qredeq  15651  eulerthlem2  15766  modprm0  15789  modprmn0modprm0  15791  coprimeprodsq2  15793  prmreclem6  15904  odmod  18229  cncrng  20040  cnsrng  20053  pcoass  23102  clmvscom  23168  dvlipcn  24048  plydivlem4  24342  quotcan  24355  aaliou3lem3  24390  ef2kpi  24522  sinperlem  24524  sinmpi  24531  cosmpi  24532  sinppi  24533  cosppi  24534  sineq0  24565  tanregt0  24577  logneg  24625  lognegb  24627  logimul  24651  tanarg  24656  logtayl  24697  cxpsqrtlem  24739  cubic2  24866  quart1  24874  log2cnv  24962  basellem1  25098  basellem3  25100  basellem5  25102  basellem8  25105  mumul  25198  chtublem  25227  perfectlem1  25245  perfectlem2  25246  perfect  25247  dchrabl  25270  bposlem6  25305  bposlem9  25308  lgsdir2lem4  25344  lgsdir2  25346  lgsdir  25348  lgsdi  25350  lgsquadlem2  25397  lgsquad2  25402  rpvmasum2  25492  mulog2sumlem1  25514  pntibndlem2  25571  pntibndlem3  25572  pntlemf  25585  nvscom  27940  ipasslem11  28151  ipblnfi  28167  hvmulcom  28356  h1de2bi  28869  homul12  29120  riesz3i  29377  riesz1  29380  kbass4  29434  sin2h  33823  heiborlem6  34037  rmym1  38177  expgrowthi  39206  expgrowth  39208  stoweidlem10  40864  perfectALTVlem1  42306  perfectALTVlem2  42307  perfectALTV  42308  tgoldbachlt  42380  2zrngnmlid2  42620