Theorem mulcom 7940

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1353   ∈ wcel 2148  (class class class)co 5875  ℂcc 7809   · cmul 7816

This theorem was proved from axioms:  ax-mulcom 7912

This theorem is referenced by:  adddir  7948  mullid  7955  mulcomi  7963  mulcomd  7979  mul12  8086  mul32  8087  mul31  8088  muladd  8341  subdir  8343  mul01  8346  mulneg2  8353  recextlem1  8608  divmulap3  8634  div23ap  8648  div13ap  8650  div12ap  8651  divmulasscomap  8653  divcanap4  8656  divmul13ap  8672  divmul24ap  8673  divcanap7  8678  div2negap  8692  prodgt02  8810  prodge02  8812  ltmul2  8813  lemul2  8814  lemul2a  8816  ltmulgt12  8822  lemulge12  8824  ltmuldiv2  8832  ltdivmul2  8835  ledivmul2  8837  lemuldiv2  8839  times2  9048  modqcyc2  10360  subsq  10627  cjmulrcl  10896  imval2  10903  abscj  11061  sqabsadd  11064  sqabssub  11065  prod3fmul  11549  prodmodclem3  11583  efcllemp  11666  efexp  11690  sinmul  11752  demoivreALT  11781  dvdsmul1  11820  odd2np1lem  11877  odd2np1  11878  opeo  11902  omeo  11903  modgcd  11992  dvdsgcd  12013  gcdmultiple  12021  coprmdvds  12092  coprmdvds2  12093  qredeq  12096  modprm0  12254  modprmn0modprm0  12256  coprimeprodsq2  12258  cncrng  13466  ef2kpi  14230  sinperlem  14232  sinmpi  14239  cosmpi  14240  sinppi  14241  cosppi  14242  cxpcom  14360  lgsdir2lem4  14435  lgsdir2  14437