Theorem mulcom 8003

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2164  (class class class)co 5919  ℂcc 7872   · cmul 7879

This theorem was proved from axioms:  ax-mulcom 7975

This theorem is referenced by:  adddir  8012  mullid  8019  mulcomi  8027  mulcomd  8043  mul12  8150  mul32  8151  mul31  8152  muladd  8405  subdir  8407  mul01  8410  mulneg2  8417  recextlem1  8672  divmulap3  8698  div23ap  8712  div13ap  8714  div12ap  8715  divmulasscomap  8717  divcanap4  8720  divmul13ap  8736  divmul24ap  8737  divcanap7  8742  div2negap  8756  prodgt02  8874  prodge02  8876  ltmul2  8877  lemul2  8878  lemul2a  8880  ltmulgt12  8886  lemulge12  8888  ltmuldiv2  8896  ltdivmul2  8899  ledivmul2  8901  lemuldiv2  8903  times2  9113  modqcyc2  10434  subsq  10720  cjmulrcl  11034  imval2  11041  abscj  11199  sqabsadd  11202  sqabssub  11203  prod3fmul  11687  prodmodclem3  11721  efcllemp  11804  efexp  11828  sinmul  11890  demoivreALT  11920  dvdsmul1  11959  odd2np1lem  12016  odd2np1  12017  opeo  12041  omeo  12042  modgcd  12131  dvdsgcd  12152  gcdmultiple  12160  coprmdvds  12233  coprmdvds2  12234  qredeq  12237  modprm0  12395  modprmn0modprm0  12397  coprimeprodsq2  12399  cncrng  14068  cnfldui  14088  ef2kpi  14982  sinperlem  14984  sinmpi  14991  cosmpi  14992  sinppi  14993  cosppi  14994  cxpcom  15112  lgsdir2lem4  15188  lgsdir2  15190  lgsquadlem2  15235  lgsquad2  15240