Theorem mulcom 7939

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1353   ∈ wcel 2148  (class class class)co 5874  ℂcc 7808   · cmul 7815

This theorem was proved from axioms:  ax-mulcom 7911

This theorem is referenced by:  adddir  7947  mullid  7954  mulcomi  7962  mulcomd  7978  mul12  8085  mul32  8086  mul31  8087  muladd  8340  subdir  8342  mul01  8345  mulneg2  8352  recextlem1  8607  divmulap3  8633  div23ap  8647  div13ap  8649  div12ap  8650  divmulasscomap  8652  divcanap4  8655  divmul13ap  8671  divmul24ap  8672  divcanap7  8677  div2negap  8691  prodgt02  8809  prodge02  8811  ltmul2  8812  lemul2  8813  lemul2a  8815  ltmulgt12  8821  lemulge12  8823  ltmuldiv2  8831  ltdivmul2  8834  ledivmul2  8836  lemuldiv2  8838  times2  9047  modqcyc2  10359  subsq  10626  cjmulrcl  10895  imval2  10902  abscj  11060  sqabsadd  11063  sqabssub  11064  prod3fmul  11548  prodmodclem3  11582  efcllemp  11665  efexp  11689  sinmul  11751  demoivreALT  11780  dvdsmul1  11819  odd2np1lem  11876  odd2np1  11877  opeo  11901  omeo  11902  modgcd  11991  dvdsgcd  12012  gcdmultiple  12020  coprmdvds  12091  coprmdvds2  12092  qredeq  12095  modprm0  12253  modprmn0modprm0  12255  coprimeprodsq2  12257  cncrng  13399  ef2kpi  14163  sinperlem  14165  sinmpi  14172  cosmpi  14173  sinppi  14174  cosppi  14175  cxpcom  14293  lgsdir2lem4  14368  lgsdir2  14370