Theorem mulcom 7903

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1348   ∈ wcel 2141  (class class class)co 5853  ℂcc 7772   · cmul 7779

This theorem was proved from axioms:  ax-mulcom 7875

This theorem is referenced by:  adddir  7911  mulid2  7918  mulcomi  7926  mulcomd  7941  mul12  8048  mul32  8049  mul31  8050  muladd  8303  subdir  8305  mul01  8308  mulneg2  8315  recextlem1  8569  divmulap3  8594  div23ap  8608  div13ap  8610  div12ap  8611  divmulasscomap  8613  divcanap4  8616  divmul13ap  8632  divmul24ap  8633  divcanap7  8638  div2negap  8652  prodgt02  8769  prodge02  8771  ltmul2  8772  lemul2  8773  lemul2a  8775  ltmulgt12  8781  lemulge12  8783  ltmuldiv2  8791  ltdivmul2  8794  ledivmul2  8796  lemuldiv2  8798  times2  9007  modqcyc2  10316  subsq  10582  cjmulrcl  10851  imval2  10858  abscj  11016  sqabsadd  11019  sqabssub  11020  prod3fmul  11504  prodmodclem3  11538  efcllemp  11621  efexp  11645  sinmul  11707  demoivreALT  11736  dvdsmul1  11775  odd2np1lem  11831  odd2np1  11832  opeo  11856  omeo  11857  modgcd  11946  dvdsgcd  11967  gcdmultiple  11975  coprmdvds  12046  coprmdvds2  12047  qredeq  12050  modprm0  12208  modprmn0modprm0  12210  coprimeprodsq2  12212  ef2kpi  13521  sinperlem  13523  sinmpi  13530  cosmpi  13531  sinppi  13532  cosppi  13533  cxpcom  13651  lgsdir2lem4  13726  lgsdir2  13728