Theorem mulcom 8008

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2167  (class class class)co 5922  ℂcc 7877   · cmul 7884

This theorem was proved from axioms:  ax-mulcom 7980

This theorem is referenced by:  adddir  8017  mullid  8024  mulcomi  8032  mulcomd  8048  mul12  8155  mul32  8156  mul31  8157  muladd  8410  subdir  8412  mul01  8415  mulneg2  8422  recextlem1  8678  divmulap3  8704  div23ap  8718  div13ap  8720  div12ap  8721  divmulasscomap  8723  divcanap4  8726  divmul13ap  8742  divmul24ap  8743  divcanap7  8748  div2negap  8762  prodgt02  8880  prodge02  8882  ltmul2  8883  lemul2  8884  lemul2a  8886  ltmulgt12  8892  lemulge12  8894  ltmuldiv2  8902  ltdivmul2  8905  ledivmul2  8907  lemuldiv2  8909  times2  9119  modqcyc2  10452  subsq  10738  cjmulrcl  11052  imval2  11059  abscj  11217  sqabsadd  11220  sqabssub  11221  prod3fmul  11706  prodmodclem3  11740  efcllemp  11823  efexp  11847  sinmul  11909  demoivreALT  11939  dvdsmul1  11978  odd2np1lem  12037  odd2np1  12038  opeo  12062  omeo  12063  modgcd  12158  dvdsgcd  12179  gcdmultiple  12187  coprmdvds  12260  coprmdvds2  12261  qredeq  12264  modprm0  12423  modprmn0modprm0  12425  coprimeprodsq2  12427  cncrng  14125  cnfldui  14145  ef2kpi  15042  sinperlem  15044  sinmpi  15051  cosmpi  15052  sinppi  15053  cosppi  15054  cxpcom  15174  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgsdir2lem4  15272  lgsdir2  15274  lgsquadlem2  15319  lgsquad2  15324