Theorem mulcom 7856

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1335   ∈ wcel 2128  (class class class)co 5821  ℂcc 7725   · cmul 7732

This theorem was proved from axioms:  ax-mulcom 7828

This theorem is referenced by:  adddir  7864  mulid2  7871  mulcomi  7879  mulcomd  7894  mul12  7999  mul32  8000  mul31  8001  muladd  8254  subdir  8256  mul01  8259  mulneg2  8266  recextlem1  8520  divmulap3  8545  div23ap  8559  div13ap  8561  div12ap  8562  divmulasscomap  8564  divcanap4  8567  divmul13ap  8583  divmul24ap  8584  divcanap7  8589  div2negap  8603  prodgt02  8719  prodge02  8721  ltmul2  8722  lemul2  8723  lemul2a  8725  ltmulgt12  8731  lemulge12  8733  ltmuldiv2  8741  ltdivmul2  8744  ledivmul2  8746  lemuldiv2  8748  times2  8957  modqcyc2  10254  subsq  10520  cjmulrcl  10782  imval2  10789  abscj  10947  sqabsadd  10950  sqabssub  10951  prod3fmul  11433  prodmodclem3  11467  efcllemp  11550  efexp  11574  sinmul  11636  demoivreALT  11665  dvdsmul1  11703  odd2np1lem  11757  odd2np1  11758  opeo  11782  omeo  11783  modgcd  11869  dvdsgcd  11890  gcdmultiple  11898  coprmdvds  11963  coprmdvds2  11964  qredeq  11967  ef2kpi  13114  sinperlem  13116  sinmpi  13123  cosmpi  13124  sinppi  13125  cosppi  13126  cxpcom  13244