Theorem mulcom 8001

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870   · cmul 7877

This theorem was proved from axioms:  ax-mulcom 7973

This theorem is referenced by:  adddir  8010  mullid  8017  mulcomi  8025  mulcomd  8041  mul12  8148  mul32  8149  mul31  8150  muladd  8403  subdir  8405  mul01  8408  mulneg2  8415  recextlem1  8670  divmulap3  8696  div23ap  8710  div13ap  8712  div12ap  8713  divmulasscomap  8715  divcanap4  8718  divmul13ap  8734  divmul24ap  8735  divcanap7  8740  div2negap  8754  prodgt02  8872  prodge02  8874  ltmul2  8875  lemul2  8876  lemul2a  8878  ltmulgt12  8884  lemulge12  8886  ltmuldiv2  8894  ltdivmul2  8897  ledivmul2  8899  lemuldiv2  8901  times2  9111  modqcyc2  10431  subsq  10717  cjmulrcl  11031  imval2  11038  abscj  11196  sqabsadd  11199  sqabssub  11200  prod3fmul  11684  prodmodclem3  11718  efcllemp  11801  efexp  11825  sinmul  11887  demoivreALT  11917  dvdsmul1  11956  odd2np1lem  12013  odd2np1  12014  opeo  12038  omeo  12039  modgcd  12128  dvdsgcd  12149  gcdmultiple  12157  coprmdvds  12230  coprmdvds2  12231  qredeq  12234  modprm0  12392  modprmn0modprm0  12394  coprimeprodsq2  12396  cncrng  14057  cnfldui  14077  ef2kpi  14941  sinperlem  14943  sinmpi  14950  cosmpi  14951  sinppi  14952  cosppi  14953  cxpcom  15071  lgsdir2lem4  15147  lgsdir2  15149