Theorem mulcom 11238

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   · cmul 11157

This theorem was proved from axioms:  ax-mulcom 11216

This theorem is referenced by:  adddir  11249  mullid  11257  mulcomi  11266  mulcomd  11279  mul12  11423  mul32  11424  mul31  11425  mul4r  11427  mul01  11437  muladd  11692  subdir  11694  mulneg2  11697  recextlem1  11890  mulcan2g  11914  divmul3  11924  div23  11938  div13  11940  div12  11941  divmulasscom  11943  divcan4  11946  divmul13  11967  divmul24  11968  divcan7  11973  div2neg  11987  prodgt02  12112  ltmul2  12115  lemul2  12117  lemul2a  12119  ltmulgt12  12125  lemulge12  12128  ltmuldiv2  12139  ltdivmul2  12142  lt2mul2div  12143  ledivmul2  12144  lemuldiv2  12146  supmul  12237  times2  12400  modcyc  13942  modcyc2  13943  modmulmodr  13974  subsq  14245  cjmulrcl  15179  imval2  15186  abscj  15314  sqabsadd  15317  sqabssub  15318  sqreulem  15394  iseraltlem2  15715  iseraltlem3  15716  climcndslem2  15882  prodfmul  15922  prodmolem3  15965  bpoly3  16090  efcllem  16109  efexp  16133  sinmul  16204  demoivreALT  16233  dvdsmul1  16311  odd2np1lem  16373  odd2np1  16374  opeo  16398  omeo  16399  modgcd  16565  bezoutlem1  16572  dvdsgcd  16577  coprmdvds  16686  coprmdvds2  16687  qredeq  16690  eulerthlem2  16815  modprm0  16838  modprmn0modprm0  16840  coprimeprodsq2  16842  prmreclem6  16954  odmod  19578  cncrng  21418  cncrngOLD  21419  cnsrng  21435  pcoass  25070  clmvscom  25136  dvlipcn  26047  plydivlem4  26352  quotcan  26365  aaliou3lem3  26400  ef2kpi  26534  sinperlem  26536  sinmpi  26543  cosmpi  26544  sinppi  26545  cosppi  26546  sineq0  26580  tanregt0  26595  logneg  26644  lognegb  26646  logimul  26670  tanarg  26675  logtayl  26716  cxpsqrtlem  26758  cxpcom  26795  cubic2  26905  quart1  26913  log2cnv  27001  basellem1  27138  basellem3  27140  basellem5  27142  basellem8  27145  mumul  27238  chtublem  27269  perfectlem1  27287  perfectlem2  27288  perfect  27289  dchrabl  27312  bposlem6  27347  bposlem9  27350  lgsdir2lem4  27386  lgsdir2  27388  lgsquadlem2  27439  lgsquad2  27444  rpvmasum2  27570  mulog2sumlem1  27592  pntibndlem2  27649  pntibndlem3  27650  pntlemf  27663  nvscom  30657  ipasslem11  30868  ipblnfi  30883  hvmulcom  31071  h1de2bi  31582  homul12  31833  riesz3i  32090  riesz1  32093  kbass4  32147  sin2h  37596  heiborlem6  37802  rmym1  42923  expgrowthi  44328  expgrowth  44330  stoweidlem10  45965  perfectALTVlem1  47645  perfectALTVlem2  47646  perfectALTV  47647  tgoldbachlt  47740  2zrngnmlid2  48100