Theorem mulcom 8161

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   · cmul 8037

This theorem was proved from axioms:  ax-mulcom 8133

This theorem is referenced by:  adddir  8170  mullid  8177  mulcomi  8185  mulcomd  8201  mul12  8308  mul32  8309  mul31  8310  muladd  8563  subdir  8565  mul01  8568  mulneg2  8575  recextlem1  8831  divmulap3  8857  div23ap  8871  div13ap  8873  div12ap  8874  divmulasscomap  8876  divcanap4  8879  divmul13ap  8895  divmul24ap  8896  divcanap7  8901  div2negap  8915  prodgt02  9033  prodge02  9035  ltmul2  9036  lemul2  9037  lemul2a  9039  ltmulgt12  9045  lemulge12  9047  ltmuldiv2  9055  ltdivmul2  9058  ledivmul2  9060  lemuldiv2  9062  times2  9272  modqcyc2  10623  subsq  10909  cjmulrcl  11452  imval2  11459  abscj  11617  sqabsadd  11620  sqabssub  11621  prod3fmul  12107  prodmodclem3  12141  efcllemp  12224  efexp  12248  sinmul  12310  demoivreALT  12340  dvdsmul1  12379  odd2np1lem  12438  odd2np1  12439  opeo  12463  omeo  12464  modgcd  12567  dvdsgcd  12588  gcdmultiple  12596  coprmdvds  12669  coprmdvds2  12670  qredeq  12673  modprm0  12832  modprmn0modprm0  12834  coprimeprodsq2  12836  cncrng  14589  cnfldui  14609  ef2kpi  15536  sinperlem  15538  sinmpi  15545  cosmpi  15546  sinppi  15547  cosppi  15548  cxpcom  15668  perfectlem1  15729  perfectlem2  15730  perfect  15731  lgsdir2lem4  15766  lgsdir2  15768  lgsquadlem2  15813  lgsquad2  15818