Theorem mulcom 11240

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098  (class class class)co 7423  ℂcc 11152   · cmul 11159

This theorem was proved from axioms:  ax-mulcom 11218

This theorem is referenced by:  adddir  11251  mullid  11259  mulcomi  11268  mulcomd  11281  mul12  11425  mul32  11426  mul31  11427  mul4r  11429  mul01  11439  muladd  11692  subdir  11694  mulneg2  11697  recextlem1  11890  mulcan2g  11914  divmul3  11924  div23  11938  div13  11940  div12  11941  divmulasscom  11943  divcan4  11946  divmul13  11964  divmul24  11965  divcan7  11970  div2neg  11984  prodgt02  12109  ltmul2  12112  lemul2  12114  lemul2a  12116  ltmulgt12  12122  lemulge12  12124  ltmuldiv2  12135  ltdivmul2  12138  lt2mul2div  12139  ledivmul2  12140  lemuldiv2  12142  supmul  12233  times2  12396  modcyc  13921  modcyc2  13922  modmulmodr  13952  subsq  14223  cjmulrcl  15144  imval2  15151  abscj  15279  sqabsadd  15282  sqabssub  15283  sqreulem  15359  iseraltlem2  15682  iseraltlem3  15683  climcndslem2  15849  prodfmul  15889  prodmolem3  15930  bpoly3  16055  efcllem  16074  efexp  16098  sinmul  16169  demoivreALT  16198  dvdsmul1  16275  odd2np1lem  16337  odd2np1  16338  opeo  16362  omeo  16363  modgcd  16528  bezoutlem1  16535  dvdsgcd  16540  coprmdvds  16649  coprmdvds2  16650  qredeq  16653  eulerthlem2  16779  modprm0  16802  modprmn0modprm0  16804  coprimeprodsq2  16806  prmreclem6  16918  odmod  19539  cncrng  21372  cncrngOLD  21373  cnsrng  21389  pcoass  25034  clmvscom  25100  dvlipcn  26010  plydivlem4  26316  quotcan  26329  aaliou3lem3  26364  ef2kpi  26498  sinperlem  26500  sinmpi  26507  cosmpi  26508  sinppi  26509  cosppi  26510  sineq0  26543  tanregt0  26558  logneg  26607  lognegb  26609  logimul  26633  tanarg  26638  logtayl  26679  cxpsqrtlem  26721  cxpcom  26758  cubic2  26868  quart1  26876  log2cnv  26964  basellem1  27101  basellem3  27103  basellem5  27105  basellem8  27108  mumul  27201  chtublem  27232  perfectlem1  27250  perfectlem2  27251  perfect  27252  dchrabl  27275  bposlem6  27310  bposlem9  27313  lgsdir2lem4  27349  lgsdir2  27351  lgsquadlem2  27402  lgsquad2  27407  rpvmasum2  27533  mulog2sumlem1  27555  pntibndlem2  27612  pntibndlem3  27613  pntlemf  27626  nvscom  30554  ipasslem11  30765  ipblnfi  30780  hvmulcom  30968  h1de2bi  31479  homul12  31730  riesz3i  31987  riesz1  31990  kbass4  32044  sin2h  37259  heiborlem6  37465  rmym1  42530  expgrowthi  43944  expgrowth  43946  stoweidlem10  45568  perfectALTVlem1  47230  perfectALTVlem2  47231  perfectALTV  47232  tgoldbachlt  47325  2zrngnmlid2  47571