Theorem mulcom 11198

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1539   ∈ wcel 2104  (class class class)co 7411  ℂcc 11110   · cmul 11117

This theorem was proved from axioms:  ax-mulcom 11176

This theorem is referenced by:  adddir  11209  mullid  11217  mulcomi  11226  mulcomd  11239  mul12  11383  mul32  11384  mul31  11385  mul4r  11387  mul01  11397  muladd  11650  subdir  11652  mulneg2  11655  recextlem1  11848  mulcan2g  11872  divmul3  11881  div23  11895  div13  11897  div12  11898  divmulasscom  11900  divcan4  11903  divmul13  11921  divmul24  11922  divcan7  11927  div2neg  11941  prodgt02  12066  ltmul2  12069  lemul2  12071  lemul2a  12073  ltmulgt12  12079  lemulge12  12081  ltmuldiv2  12092  ltdivmul2  12095  lt2mul2div  12096  ledivmul2  12097  lemuldiv2  12099  supmul  12190  times2  12353  modcyc  13875  modcyc2  13876  modmulmodr  13906  subsq  14178  cjmulrcl  15095  imval2  15102  abscj  15230  sqabsadd  15233  sqabssub  15234  sqreulem  15310  iseraltlem2  15633  iseraltlem3  15634  climcndslem2  15800  prodfmul  15840  prodmolem3  15881  bpoly3  16006  efcllem  16025  efexp  16048  sinmul  16119  demoivreALT  16148  dvdsmul1  16225  odd2np1lem  16287  odd2np1  16288  opeo  16312  omeo  16313  modgcd  16478  bezoutlem1  16485  dvdsgcd  16490  coprmdvds  16594  coprmdvds2  16595  qredeq  16598  eulerthlem2  16719  modprm0  16742  modprmn0modprm0  16744  coprimeprodsq2  16746  prmreclem6  16858  odmod  19455  cncrng  21166  cnsrng  21179  pcoass  24771  clmvscom  24837  dvlipcn  25746  plydivlem4  26045  quotcan  26058  aaliou3lem3  26093  ef2kpi  26224  sinperlem  26226  sinmpi  26233  cosmpi  26234  sinppi  26235  cosppi  26236  sineq0  26269  tanregt0  26284  logneg  26332  lognegb  26334  logimul  26358  tanarg  26363  logtayl  26404  cxpsqrtlem  26446  cxpcom  26483  cubic2  26589  quart1  26597  log2cnv  26685  basellem1  26821  basellem3  26823  basellem5  26825  basellem8  26828  mumul  26921  chtublem  26950  perfectlem1  26968  perfectlem2  26969  perfect  26970  dchrabl  26993  bposlem6  27028  bposlem9  27031  lgsdir2lem4  27067  lgsdir2  27069  lgsquadlem2  27120  lgsquad2  27125  rpvmasum2  27251  mulog2sumlem1  27273  pntibndlem2  27330  pntibndlem3  27331  pntlemf  27344  nvscom  30149  ipasslem11  30360  ipblnfi  30375  hvmulcom  30563  h1de2bi  31074  homul12  31325  riesz3i  31582  riesz1  31585  kbass4  31639  gg-cncrng  35486  sin2h  36781  heiborlem6  36987  rmym1  41976  expgrowthi  43394  expgrowth  43396  stoweidlem10  45024  perfectALTVlem1  46687  perfectALTVlem2  46688  perfectALTV  46689  tgoldbachlt  46782  2zrngnmlid2  46937