Theorem mulcom 11089

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001   · cmul 11008

This theorem was proved from axioms:  ax-mulcom 11067

This theorem is referenced by:  adddir  11100  mullid  11108  mulcomi  11117  mulcomd  11130  mul12  11275  mul32  11276  mul31  11277  mul4r  11279  mul01  11289  muladd  11546  subdir  11548  mulneg2  11551  recextlem1  11744  mulcan2g  11768  divmul3  11778  div23  11792  div13  11794  div12  11795  divmulasscom  11797  divcan4  11800  divmul13  11821  divmul24  11822  divcan7  11827  div2neg  11841  prodgt02  11966  ltmul2  11969  lemul2  11971  lemul2a  11973  ltmulgt12  11979  lemulge12  11982  ltmuldiv2  11993  ltdivmul2  11996  lt2mul2div  11997  ledivmul2  11998  lemuldiv2  12000  supmul  12091  times2  12254  modcyc  13807  modcyc2  13808  modmulmodr  13841  subsq  14114  cjmulrcl  15048  imval2  15055  abscj  15183  sqabsadd  15186  sqabssub  15187  sqreulem  15264  iseraltlem2  15587  iseraltlem3  15588  climcndslem2  15754  prodfmul  15794  prodmolem3  15837  bpoly3  15962  efcllem  15981  efexp  16007  sinmul  16078  demoivreALT  16107  dvdsmul1  16185  odd2np1lem  16248  odd2np1  16249  opeo  16273  omeo  16274  modgcd  16440  bezoutlem1  16447  dvdsgcd  16452  coprmdvds  16561  coprmdvds2  16562  qredeq  16565  eulerthlem2  16690  modprm0  16714  modprmn0modprm0  16716  coprimeprodsq2  16718  prmreclem6  16830  odmod  19456  cncrng  21323  cncrngOLD  21324  cnsrng  21340  pcoass  24949  clmvscom  25015  dvlipcn  25924  plydivlem4  26229  quotcan  26242  aaliou3lem3  26277  ef2kpi  26412  sinperlem  26414  sinmpi  26421  cosmpi  26422  sinppi  26423  cosppi  26424  sineq0  26458  tanregt0  26473  logneg  26522  lognegb  26524  logimul  26548  tanarg  26553  logtayl  26594  cxpsqrtlem  26636  cxpcom  26673  cubic2  26783  quart1  26791  log2cnv  26879  basellem1  27016  basellem3  27018  basellem5  27020  basellem8  27023  mumul  27116  chtublem  27147  perfectlem1  27165  perfectlem2  27166  perfect  27167  dchrabl  27190  bposlem6  27225  bposlem9  27228  lgsdir2lem4  27264  lgsdir2  27266  lgsquadlem2  27317  lgsquad2  27322  rpvmasum2  27448  mulog2sumlem1  27470  pntibndlem2  27527  pntibndlem3  27528  pntlemf  27541  nvscom  30604  ipasslem11  30815  ipblnfi  30830  hvmulcom  31018  h1de2bi  31529  homul12  31780  riesz3i  32037  riesz1  32040  kbass4  32094  sin2h  37649  heiborlem6  37855  rmym1  42967  expgrowthi  44365  expgrowth  44367  stoweidlem10  46047  perfectALTVlem1  47751  perfectALTVlem2  47752  perfectALTV  47753  tgoldbachlt  47846  2zrngnmlid2  48287