Theorem mulcom 7525

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1290   ∈ wcel 1439  (class class class)co 5666  ℂcc 7402   · cmul 7409

This theorem was proved from axioms:  ax-mulcom 7500

This theorem is referenced by:  adddir  7533  mulid2  7540  mulcomi  7548  mulcomd  7563  mul12  7665  mul32  7666  mul31  7667  muladd  7916  subdir  7918  mul01  7921  mulneg2  7928  recextlem1  8174  divmulap3  8198  div23ap  8212  div13ap  8214  div12ap  8215  divmulasscomap  8217  divcanap4  8220  divmul13ap  8236  divmul24ap  8237  divcanap7  8242  div2negap  8256  prodgt02  8368  prodge02  8370  ltmul2  8371  lemul2  8372  lemul2a  8374  ltmulgt12  8380  lemulge12  8382  ltmuldiv2  8390  ltdivmul2  8393  ledivmul2  8395  lemuldiv2  8397  times2  8599  modqcyc2  9821  subsq  10115  cjmulrcl  10375  imval2  10382  abscj  10539  sqabsadd  10542  sqabssub  10543  efcllemp  11002  efexp  11026  sinmul  11089  demoivreALT  11117  dvdsmul1  11150  odd2np1lem  11204  odd2np1  11205  opeo  11229  omeo  11230  modgcd  11314  dvdsgcd  11333  gcdmultiple  11341  coprmdvds  11406  coprmdvds2  11407  qredeq  11410