Theorem mulcom 8298

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1402   ∈ wcel 2209  (class class class)co 6075  ℂcc 8167   · cmul 8174

This theorem was proved from axioms:  ax-mulcom 8270

This theorem is referenced by:  adddir  8307  mullid  8314  mulcomi  8322  mulcomd  8337  mul12  8445  mul32  8446  mul31  8447  muladd  8701  subdir  8703  mul01  8706  mulneg2  8713  recextlem1  8969  divmulap3  8997  div23ap  9011  div13ap  9013  div12ap  9014  divmulasscomap  9016  divcanap4  9019  divmul13ap  9035  divmul24ap  9036  divcanap7  9041  div2negap  9055  prodgt02  9173  prodge02  9175  ltmul2  9176  lemul2  9177  lemul2a  9179  ltmulgt12  9185  lemulge12  9187  ltmuldiv2  9195  ltdivmul2  9198  ledivmul2  9200  lemuldiv2  9202  times2  9412  modqcyc2  10775  subsq  11061  cjmulrcl  11630  imval2  11637  abscj  11796  sqabsadd  11799  sqabssub  11800  prod3fmul  12286  prodmodclem3  12320  efcllemp  12403  efexp  12427  sinmul  12489  demoivreALT  12519  dvdsmul1  12558  odd2np1lem  12617  odd2np1  12618  opeo  12642  omeo  12643  modgcd  12746  dvdsgcd  12767  gcdmultiple  12775  coprmdvds  12848  coprmdvds2  12849  qredeq  12852  modprm0  13011  modprmn0modprm0  13013  coprimeprodsq2  13015  cncrng  14878  cnfldui  14896  ef2kpi  15830  sinperlem  15832  sinmpi  15839  cosmpi  15840  sinppi  15841  cosppi  15842  cxpcom  15963  perfectlem1  16027  perfectlem2  16028  perfect  16029  lgsdir2lem4  16064  lgsdir2  16066  lgsquadlem2  16111  lgsquad2  16116