Theorem mulcom 8025

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7894   · cmul 7901

This theorem was proved from axioms:  ax-mulcom 7997

This theorem is referenced by:  adddir  8034  mullid  8041  mulcomi  8049  mulcomd  8065  mul12  8172  mul32  8173  mul31  8174  muladd  8427  subdir  8429  mul01  8432  mulneg2  8439  recextlem1  8695  divmulap3  8721  div23ap  8735  div13ap  8737  div12ap  8738  divmulasscomap  8740  divcanap4  8743  divmul13ap  8759  divmul24ap  8760  divcanap7  8765  div2negap  8779  prodgt02  8897  prodge02  8899  ltmul2  8900  lemul2  8901  lemul2a  8903  ltmulgt12  8909  lemulge12  8911  ltmuldiv2  8919  ltdivmul2  8922  ledivmul2  8924  lemuldiv2  8926  times2  9136  modqcyc2  10469  subsq  10755  cjmulrcl  11069  imval2  11076  abscj  11234  sqabsadd  11237  sqabssub  11238  prod3fmul  11723  prodmodclem3  11757  efcllemp  11840  efexp  11864  sinmul  11926  demoivreALT  11956  dvdsmul1  11995  odd2np1lem  12054  odd2np1  12055  opeo  12079  omeo  12080  modgcd  12183  dvdsgcd  12204  gcdmultiple  12212  coprmdvds  12285  coprmdvds2  12286  qredeq  12289  modprm0  12448  modprmn0modprm0  12450  coprimeprodsq2  12452  cncrng  14201  cnfldui  14221  ef2kpi  15126  sinperlem  15128  sinmpi  15135  cosmpi  15136  sinppi  15137  cosppi  15138  cxpcom  15258  perfectlem1  15319  perfectlem2  15320  perfect  15321  lgsdir2lem4  15356  lgsdir2  15358  lgsquadlem2  15403  lgsquad2  15408