Theorem mulcom 11154

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

Assertion

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

Proof of Theorem mulcom

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   · cmul 11073

This theorem was proved from axioms:  ax-mulcom 11132

This theorem is referenced by:  adddir  11165  mullid  11173  mulcomi  11182  mulcomd  11195  mul12  11339  mul32  11340  mul31  11341  mul4r  11343  mul01  11353  muladd  11610  subdir  11612  mulneg2  11615  recextlem1  11808  mulcan2g  11832  divmul3  11842  div23  11856  div13  11858  div12  11859  divmulasscom  11861  divcan4  11864  divmul13  11885  divmul24  11886  divcan7  11891  div2neg  11905  prodgt02  12030  ltmul2  12033  lemul2  12035  lemul2a  12037  ltmulgt12  12043  lemulge12  12046  ltmuldiv2  12057  ltdivmul2  12060  lt2mul2div  12061  ledivmul2  12062  lemuldiv2  12064  supmul  12155  times2  12318  modcyc  13868  modcyc2  13869  modmulmodr  13902  subsq  14175  cjmulrcl  15110  imval2  15117  abscj  15245  sqabsadd  15248  sqabssub  15249  sqreulem  15326  iseraltlem2  15649  iseraltlem3  15650  climcndslem2  15816  prodfmul  15856  prodmolem3  15899  bpoly3  16024  efcllem  16043  efexp  16069  sinmul  16140  demoivreALT  16169  dvdsmul1  16247  odd2np1lem  16310  odd2np1  16311  opeo  16335  omeo  16336  modgcd  16502  bezoutlem1  16509  dvdsgcd  16514  coprmdvds  16623  coprmdvds2  16624  qredeq  16627  eulerthlem2  16752  modprm0  16776  modprmn0modprm0  16778  coprimeprodsq2  16780  prmreclem6  16892  odmod  19476  cncrng  21300  cncrngOLD  21301  cnsrng  21317  pcoass  24924  clmvscom  24990  dvlipcn  25899  plydivlem4  26204  quotcan  26217  aaliou3lem3  26252  ef2kpi  26387  sinperlem  26389  sinmpi  26396  cosmpi  26397  sinppi  26398  cosppi  26399  sineq0  26433  tanregt0  26448  logneg  26497  lognegb  26499  logimul  26523  tanarg  26528  logtayl  26569  cxpsqrtlem  26611  cxpcom  26648  cubic2  26758  quart1  26766  log2cnv  26854  basellem1  26991  basellem3  26993  basellem5  26995  basellem8  26998  mumul  27091  chtublem  27122  perfectlem1  27140  perfectlem2  27141  perfect  27142  dchrabl  27165  bposlem6  27200  bposlem9  27203  lgsdir2lem4  27239  lgsdir2  27241  lgsquadlem2  27292  lgsquad2  27297  rpvmasum2  27423  mulog2sumlem1  27445  pntibndlem2  27502  pntibndlem3  27503  pntlemf  27516  nvscom  30558  ipasslem11  30769  ipblnfi  30784  hvmulcom  30972  h1de2bi  31483  homul12  31734  riesz3i  31991  riesz1  31994  kbass4  32048  sin2h  37604  heiborlem6  37810  rmym1  42924  expgrowthi  44322  expgrowth  44324  stoweidlem10  46008  perfectALTVlem1  47722  perfectALTVlem2  47723  perfectALTV  47724  tgoldbachlt  47817  2zrngnmlid2  48245