Theorem mulcom 10234

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1632   ∈ wcel 2139  (class class class)co 6814  ℂcc 10146   · cmul 10153

This theorem was proved from axioms:  ax-mulcom 10212

This theorem is referenced by:  adddir  10243  mulid2  10250  mulcomi  10258  mulcomd  10273  mul12  10414  mul32  10415  mul31  10416  mul01  10427  muladd  10674  subdir  10676  mulneg2  10679  recextlem1  10869  mulcan2g  10893  divmul3  10902  div23  10916  div13  10918  div12  10919  divmulasscom  10921  divcan4  10924  divmul13  10940  divmul24  10941  divcan7  10946  div2neg  10960  prodgt02  11081  prodge02  11083  ltmul2  11086  lemul2  11088  lemul2a  11090  ltmulgt12  11096  lemulge12  11098  ltmuldiv2  11109  ltdivmul2  11112  lt2mul2div  11113  ledivmul2  11114  lemuldiv2  11116  supmul  11207  times2  11358  modcyc  12919  modcyc2  12920  modmulmodr  12950  subsq  13186  cjmulrcl  14103  imval2  14110  abscj  14238  sqabsadd  14241  sqabssub  14242  sqreulem  14318  iseraltlem2  14632  iseraltlem3  14633  climcndslem2  14801  prodfmul  14841  prodmolem3  14882  bpoly3  15008  efcllem  15027  efexp  15050  sinmul  15121  demoivreALT  15150  dvdsmul1  15225  odd2np1lem  15286  odd2np1  15287  opeo  15311  omeo  15312  modgcd  15475  bezoutlem1  15478  dvdsgcd  15483  gcdmultiple  15491  coprmdvds  15588  coprmdvdsOLD  15589  coprmdvds2  15590  qredeq  15593  eulerthlem2  15709  modprm0  15732  modprmn0modprm0  15734  coprimeprodsq2  15736  prmreclem6  15847  odmod  18185  cncrng  19989  cnsrng  20002  pcoass  23044  clmvscom  23110  dvlipcn  23976  plydivlem4  24270  quotcan  24283  aaliou3lem3  24318  ef2kpi  24450  sinperlem  24452  sinmpi  24459  cosmpi  24460  sinppi  24461  cosppi  24462  sineq0  24493  tanregt0  24505  logneg  24554  lognegb  24556  logimul  24580  tanarg  24585  logtayl  24626  cxpsqrtlem  24668  cubic2  24795  quart1  24803  log2cnv  24891  basellem1  25027  basellem3  25029  basellem5  25031  basellem8  25034  mumul  25127  chtublem  25156  perfectlem1  25174  perfectlem2  25175  perfect  25176  dchrabl  25199  bposlem6  25234  bposlem9  25237  lgsdir2lem4  25273  lgsdir2  25275  lgsdir  25277  lgsdi  25279  lgsquadlem2  25326  lgsquad2  25331  rpvmasum2  25421  mulog2sumlem1  25443  pntibndlem2  25500  pntibndlem3  25501  pntlemf  25514  nvscom  27814  ipasslem11  28025  ipblnfi  28041  hvmulcom  28230  h1de2bi  28743  homul12  28994  riesz3i  29251  riesz1  29254  kbass4  29308  sin2h  33730  heiborlem6  33946  rmym1  38020  expgrowthi  39052  expgrowth  39054  stoweidlem10  40748  perfectALTVlem1  42158  perfectALTVlem2  42159  perfectALTV  42160  tgoldbachlt  42232  tgoldbachltOLD  42238  2zrngnmlid2  42479