Theorem mulcom 8027

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   · cmul 7903

This theorem was proved from axioms:  ax-mulcom 7999

This theorem is referenced by:  adddir  8036  mullid  8043  mulcomi  8051  mulcomd  8067  mul12  8174  mul32  8175  mul31  8176  muladd  8429  subdir  8431  mul01  8434  mulneg2  8441  recextlem1  8697  divmulap3  8723  div23ap  8737  div13ap  8739  div12ap  8740  divmulasscomap  8742  divcanap4  8745  divmul13ap  8761  divmul24ap  8762  divcanap7  8767  div2negap  8781  prodgt02  8899  prodge02  8901  ltmul2  8902  lemul2  8903  lemul2a  8905  ltmulgt12  8911  lemulge12  8913  ltmuldiv2  8921  ltdivmul2  8924  ledivmul2  8926  lemuldiv2  8928  times2  9138  modqcyc2  10471  subsq  10757  cjmulrcl  11071  imval2  11078  abscj  11236  sqabsadd  11239  sqabssub  11240  prod3fmul  11725  prodmodclem3  11759  efcllemp  11842  efexp  11866  sinmul  11928  demoivreALT  11958  dvdsmul1  11997  odd2np1lem  12056  odd2np1  12057  opeo  12081  omeo  12082  modgcd  12185  dvdsgcd  12206  gcdmultiple  12214  coprmdvds  12287  coprmdvds2  12288  qredeq  12291  modprm0  12450  modprmn0modprm0  12452  coprimeprodsq2  12454  cncrng  14203  cnfldui  14223  ef2kpi  15150  sinperlem  15152  sinmpi  15159  cosmpi  15160  sinppi  15161  cosppi  15162  cxpcom  15282  perfectlem1  15343  perfectlem2  15344  perfect  15345  lgsdir2lem4  15380  lgsdir2  15382  lgsquadlem2  15427  lgsquad2  15432