Theorem mulcom 7749

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331   ∈ wcel 1480  (class class class)co 5774  ℂcc 7618   · cmul 7625

This theorem was proved from axioms:  ax-mulcom 7721

This theorem is referenced by:  adddir  7757  mulid2  7764  mulcomi  7772  mulcomd  7787  mul12  7891  mul32  7892  mul31  7893  muladd  8146  subdir  8148  mul01  8151  mulneg2  8158  recextlem1  8412  divmulap3  8437  div23ap  8451  div13ap  8453  div12ap  8454  divmulasscomap  8456  divcanap4  8459  divmul13ap  8475  divmul24ap  8476  divcanap7  8481  div2negap  8495  prodgt02  8611  prodge02  8613  ltmul2  8614  lemul2  8615  lemul2a  8617  ltmulgt12  8623  lemulge12  8625  ltmuldiv2  8633  ltdivmul2  8636  ledivmul2  8638  lemuldiv2  8640  times2  8849  modqcyc2  10133  subsq  10399  cjmulrcl  10659  imval2  10666  abscj  10824  sqabsadd  10827  sqabssub  10828  prod3fmul  11310  prodmodclem3  11344  efcllemp  11364  efexp  11388  sinmul  11451  demoivreALT  11480  dvdsmul1  11515  odd2np1lem  11569  odd2np1  11570  opeo  11594  omeo  11595  modgcd  11679  dvdsgcd  11700  gcdmultiple  11708  coprmdvds  11773  coprmdvds2  11774  qredeq  11777  ef2kpi  12887  sinperlem  12889  sinmpi  12896  cosmpi  12897  sinppi  12898  cosppi  12899