Theorem mulid1d 9649

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
addcld.1	|- ( ph -> A e. CC )

Assertion

Ref	Expression
mulid1d	|- ( ph -> ( A x. 1 ) = A )

Proof of Theorem mulid1d

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		mulid1 9629	. 2 |- ( A e. CC -> ( A x. 1 ) = A )
3	1, 2	syl 17	1 |- ( ph -> ( A x. 1 ) = A )

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1867  (class class class)co 6296   CCcc 9526   1c1 9529   x. cmul 9533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-resscn 9585  ax-1cn 9586  ax-icn 9587  ax-addcl 9588  ax-mulcl 9590  ax-mulcom 9592  ax-mulass 9594  ax-distr 9595  ax-1rid 9598  ax-cnre 9601

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-iota 5556  df-fv 5600  df-ov 6299

This theorem is referenced by:  muladd11  9792  divrec  10275  diveq1  10290  conjmul  10313  divelunit  11761  modid  12107  expadd  12300  leexp2r  12316  nnlesq  12364  faclbnd  12461  faclbnd2  12462  faclbnd4lem3  12466  faclbnd6  12470  facavg  12472  bcn0  12481  bcn1  12484  hashf1lem2  12603  hashfac  12605  reccn2  13627  iseraltlem2  13716  iseraltlem3  13717  binom11  13857  harmonic  13884  arisum2  13886  trireciplem  13887  geoserg  13891  cvgrat  13906  fprodsplit  13987  fprodle  14017  fsumcube  14080  efzval  14123  tanhlt1  14181  tanaddlem  14187  tanadd  14188  cos01gt0  14212  absef  14218  1dvds  14284  3dvds  14336  bitsfzo  14372  bitsmod  14373  gcdmultiple  14478  sqgcd  14486  lcm1  14535  coprmdvds  14619  qredeu  14624  phiprmpw  14682  coprimeprodsq  14711  pc2dvds  14780  sumhash  14793  fldivp1  14794  pcfaclem  14795  prmpwdvds  14800  prmreclem1  14812  vdwlem3  14885  vdwlem9  14891  prmop1  14948  sylow2a  17199  odadd  17416  zsssubrg  18954  zringcyg  18984  prmirredlem  18988  mulgrhm2  18994  znrrg  19060  icopnfcnv  21859  icopnfhmeo  21860  lebnumii  21883  reparphti  21914  itg2const  22572  itg2monolem3  22584  bddibl  22671  dveflem  22805  mvth  22818  dvlipcn  22820  dvivthlem1  22834  dvfsumle  22847  dvfsumabs  22849  dvfsumlem2  22853  plyconst  23025  plyeq0lem  23029  plyco  23060  0dgrb  23065  coefv0  23067  vieta1  23130  aaliou3lem2  23161  tayl0  23179  taylply2  23185  dvtaylp  23187  taylthlem2  23191  radcnvlem1  23230  abelthlem1  23248  abelthlem2  23249  abelthlem3  23250  abelthlem7  23255  abelthlem8  23256  abelthlem9  23257  efper  23296  tangtx  23322  eflogeq  23413  logdivlti  23431  logcnlem4  23452  advlogexp  23462  cxpmul2  23496  dvcxp2  23543  cxpaddle  23554  cxpeq  23559  loglesqrt  23560  relogbexp  23579  ang180lem5  23604  isosctrlem2  23610  isosctrlem3  23611  heron  23626  2efiatan  23706  dvatan  23723  leibpi  23730  birthdaylem3  23741  jensenlem2  23775  logdiflbnd  23782  harmonicbnd4  23798  lgamgulmlem2  23817  lgamcvg2  23842  wilthlem2  23856  ftalem5  23863  basellem2  23868  basellem5  23871  basellem8  23874  0sgm  23931  muinv  23982  chpub  24008  logfaclbnd  24010  logexprlim  24013  dchrsum2  24056  sumdchr2  24058  bposlem1  24072  bposlem2  24073  bposlem5  24076  lgsquad2lem1  24146  lgsquad3  24149  2sqlem6  24157  2sqlem8  24160  chtppilim  24173  vmadivsum  24180  dchrisumlem1  24187  dchrisum0flblem1  24206  rpvmasum2  24210  dchrisum0re  24211  dchrisum0lem2a  24215  dchrisum0lem3  24217  rpvmasum  24224  mudivsum  24228  mulogsumlem  24229  vmalogdivsum2  24236  pntrsumo1  24263  pntrlog2bndlem2  24276  pntrlog2bndlem4  24278  pntrlog2bndlem5  24279  pntibndlem2  24289  pntlemc  24293  pntlemf  24303  ostth2lem2  24332  ostth2lem3  24333  ostth2lem4  24334  ostth2  24335  ostth3  24336  ttgcontlem1  24758  axpaschlem  24813  axcontlem2  24838  axcontlem4  24840  axcontlem8  24844  nmoub3i  26256  ubthlem2  26355  htthlem  26402  nmcexi  27511  nmopcoadji  27586  branmfn  27590  rearchi  28441  madjusmdetlem4  28492  ccatmulgnn0dir  29213  ofcccat  29215  subfacval2  29695  cvmliftlem2  29794  snmlff  29837  sinccvglem  30101  muls1d  30152  bcprod  30158  faclimlem1  30163  faclimlem2  30164  faclim2  30168  poimirlem29  31673  poimirlem30  31674  poimirlem31  31675  poimirlem32  31676  itg2addnclem  31697  areacirclem1  31736  areacirclem4  31739  cntotbnd  31832  irrapxlem1  35376  irrapxlem4  35379  pell1qrgaplem  35429  reglogexpbas  35455  rmspecsqrtnq  35464  rmspecfund  35467  rmxy1  35480  rmxp1  35490  rmyp1  35491  rmxm1  35492  jm2.17a  35520  jm2.18  35553  jm2.23  35561  jm2.25  35564  jm2.16nn0  35569  relexpmulnn  35944  int-mul11d  36270  nzprmdif  36309  expgrowthi  36323  expgrowth  36325  binomcxplemdvbinom  36343  binomcxplemnotnn0  36346  fmul01  37234  fmul01lt1lem1  37238  m1expevenOLD  37246  0ellimcdiv  37306  dvxpaek  37388  dvnxpaek  37390  itgiccshift  37430  itgperiod  37431  itgsbtaddcnst  37432  stoweidlem11  37444  stoweidlem26  37459  stoweidlem38  37472  wallispilem4  37503  stirlinglem1  37509  stirlinglem3  37511  stirlinglem6  37514  stirlinglem7  37515  stirlinglem8  37516  stirlinglem10  37518  stirlinglem12  37520  dirkertrigeqlem3  37535  dirkertrigeq  37536  dirkercncflem1  37538  dirkercncflem2  37539  fourierdlem28  37570  fourierdlem30  37572  fourierdlem39  37581  fourierdlem47  37589  fourierdlem60  37602  fourierdlem61  37603  fourierdlem73  37615  fourierdlem83  37625  fourierdlem87  37629  etransclem14  37684  etransclem24  37694  etransclem25  37695  etransclem35  37705  logblt1b  39149  nn0sumshdiglem2  39207