Theorem mulcom 11112

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   · cmul 11031

This theorem was proved from axioms:  ax-mulcom 11090

This theorem is referenced by:  adddir  11123  mullid  11131  mulcomi  11140  mulcomd  11153  mul12  11298  mul32  11299  mul31  11300  mul4r  11302  mul01  11312  muladd  11569  subdir  11571  mulneg2  11574  recextlem1  11767  mulcan2g  11791  divmul3  11801  div23  11815  div13  11817  div12  11818  divmulasscom  11820  divcan4  11823  divmul13  11844  divmul24  11845  divcan7  11850  div2neg  11864  prodgt02  11989  ltmul2  11992  lemul2  11994  lemul2a  11996  ltmulgt12  12002  lemulge12  12005  ltmuldiv2  12016  ltdivmul2  12019  lt2mul2div  12020  ledivmul2  12021  lemuldiv2  12023  supmul  12114  times2  12277  modcyc  13826  modcyc2  13827  modmulmodr  13860  subsq  14133  cjmulrcl  15067  imval2  15074  abscj  15202  sqabsadd  15205  sqabssub  15206  sqreulem  15283  iseraltlem2  15606  iseraltlem3  15607  climcndslem2  15773  prodfmul  15813  prodmolem3  15856  bpoly3  15981  efcllem  16000  efexp  16026  sinmul  16097  demoivreALT  16126  dvdsmul1  16204  odd2np1lem  16267  odd2np1  16268  opeo  16292  omeo  16293  modgcd  16459  bezoutlem1  16466  dvdsgcd  16471  coprmdvds  16580  coprmdvds2  16581  qredeq  16584  eulerthlem2  16709  modprm0  16733  modprmn0modprm0  16735  coprimeprodsq2  16737  prmreclem6  16849  odmod  19475  cncrng  21343  cncrngOLD  21344  cnsrng  21360  pcoass  24980  clmvscom  25046  dvlipcn  25955  plydivlem4  26260  quotcan  26273  aaliou3lem3  26308  ef2kpi  26443  sinperlem  26445  sinmpi  26452  cosmpi  26453  sinppi  26454  cosppi  26455  sineq0  26489  tanregt0  26504  logneg  26553  lognegb  26555  logimul  26579  tanarg  26584  logtayl  26625  cxpsqrtlem  26667  cxpcom  26704  cubic2  26814  quart1  26822  log2cnv  26910  basellem1  27047  basellem3  27049  basellem5  27051  basellem8  27054  mumul  27147  chtublem  27178  perfectlem1  27196  perfectlem2  27197  perfect  27198  dchrabl  27221  bposlem6  27256  bposlem9  27259  lgsdir2lem4  27295  lgsdir2  27297  lgsquadlem2  27348  lgsquad2  27353  rpvmasum2  27479  mulog2sumlem1  27501  pntibndlem2  27558  pntibndlem3  27559  pntlemf  27572  nvscom  30704  ipasslem11  30915  ipblnfi  30930  hvmulcom  31118  h1de2bi  31629  homul12  31880  riesz3i  32137  riesz1  32140  kbass4  32194  sin2h  37807  heiborlem6  38013  rmym1  43173  expgrowthi  44570  expgrowth  44572  stoweidlem10  46250  perfectALTVlem1  47963  perfectALTVlem2  47964  perfectALTV  47965  tgoldbachlt  48058  2zrngnmlid2  48499