Theorem mulcom 8116

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1395   ∈ wcel 2200  (class class class)co 5994  ℂcc 7985   · cmul 7992

This theorem was proved from axioms:  ax-mulcom 8088

This theorem is referenced by:  adddir  8125  mullid  8132  mulcomi  8140  mulcomd  8156  mul12  8263  mul32  8264  mul31  8265  muladd  8518  subdir  8520  mul01  8523  mulneg2  8530  recextlem1  8786  divmulap3  8812  div23ap  8826  div13ap  8828  div12ap  8829  divmulasscomap  8831  divcanap4  8834  divmul13ap  8850  divmul24ap  8851  divcanap7  8856  div2negap  8870  prodgt02  8988  prodge02  8990  ltmul2  8991  lemul2  8992  lemul2a  8994  ltmulgt12  9000  lemulge12  9002  ltmuldiv2  9010  ltdivmul2  9013  ledivmul2  9015  lemuldiv2  9017  times2  9227  modqcyc2  10569  subsq  10855  cjmulrcl  11384  imval2  11391  abscj  11549  sqabsadd  11552  sqabssub  11553  prod3fmul  12038  prodmodclem3  12072  efcllemp  12155  efexp  12179  sinmul  12241  demoivreALT  12271  dvdsmul1  12310  odd2np1lem  12369  odd2np1  12370  opeo  12394  omeo  12395  modgcd  12498  dvdsgcd  12519  gcdmultiple  12527  coprmdvds  12600  coprmdvds2  12601  qredeq  12604  modprm0  12763  modprmn0modprm0  12765  coprimeprodsq2  12767  cncrng  14518  cnfldui  14538  ef2kpi  15465  sinperlem  15467  sinmpi  15474  cosmpi  15475  sinppi  15476  cosppi  15477  cxpcom  15597  perfectlem1  15658  perfectlem2  15659  perfect  15660  lgsdir2lem4  15695  lgsdir2  15697  lgsquadlem2  15742  lgsquad2  15747