Theorem mulcom 11287

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

Assertion

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

Proof of Theorem mulcom

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  (class class class)co 7421  ℂcc 11199   · cmul 11206

This proof depends on axioms:  ax-mulcom 11265

This theorem is used by:  adddir  11298  mullid  11308  mulcomi  11318  mulcomd  11331  mul12  11476  mul32  11477  mul31  11478  mul4r  11480  mul01  11490  muladd  11749  subdir  11751  mulneg2  11754  recextlem1  11947  mulcan2g  11971  divmul3  11980  div23  11994  div13  11996  div12  11997  divmulasscom  11999  divcan4  12002  divmul13  12021  divmul24  12022  divcan7  12027  div2neg  12041  prodgt02  12166  ltmul2  12169  lemul2  12171  lemul2a  12173  ltmulgt12  12178  lemulge12  12181  ltmuldiv2  12192  ltdivmul2  12195  lt2mul2div  12196  ledivmul2  12197  lemuldiv2  12199  supmul  12290  times2  12480  modcyc  14047  modcyc2  14048  modmulmodr  14081  subsq  14355  cjmulrcl  15312  imval2  15319  abscj  15447  sqabsadd  15450  sqabssub  15451  sqreulem  15528  iseraltlem2  15851  iseraltlem3  15852  climcndslem2  16020  prodfmul  16060  prodmolem3  16101  bpoly3  16225  efcllem  16244  efexp  16270  sinmul  16341  demoivreALT  16370  dvdsmul1  16448  odd2np1lem  16511  odd2np1  16512  opeo  16536  omeo  16537  modgcd  16706  bezoutlem1  16713  dvdsgcd  16718  coprmdvds  16829  coprmdvds2  16830  qredeq  16833  eulerthlem2  16960  modprm0  16984  modprmn0modprm0  16986  coprimeprodsq2  16988  prmreclem6  17100  odmod  19761  cncrng  21700  cnsrng  21713  pcoass  25346  clmvscom  25412  dvlipcn  26315  plydivlem4  26618  quotcan  26633  aaliou3lem3  26672  ef2kpi  26808  sinperlem  26810  sinmpi  26817  cosmpi  26818  sinppi  26819  cosppi  26820  sineq0  26853  tanregt0  26868  logneg  26917  lognegb  26919  logimul  26943  tanarg  26948  logtayl  26989  cxpsqrtlem  27031  cxpcom  27068  cubic2  27177  quart1  27185  log2cnv  27273  basellem1  27409  basellem3  27411  basellem5  27413  mumul  27509  chtublem  27539  perfectlem1  27557  perfectlem2  27558  perfect  27559  dchrabl  27582  bposlem6  27617  bposlem9  27620  lgsdir2lem4  27656  lgsdir2  27658  lgsquadlem2  27709  lgsquad2  27714  rpvmasum2  27840  mulog2sumlem1  27862  pntibndlem2  27919  pntibndlem3  27920  pntlemf  27933  nvscom  31232  ipasslem11  31443  ipblnfi  31458  hvmulcom  31646  h1de2bi  32157  homul12  32408  riesz3i  32665  riesz1  32668  kbass4  32722  sin2h  38535  heiborlem6  38752  rmym1  43943  expgrowthi  45318  expgrowth  45320  stoweidlem10  47021  perfectALTVlem1  48820  perfectALTVlem2  48821  perfectALTV  48822  tgoldbachlt  48915  2zrngnmlid2  49355