Theorem mulid1d 9660

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 9640	. 2 |- ( A e. CC -> ( A x. 1 ) = A )
3	1, 2	syl 17	1 |- ( ph -> ( A x. 1 ) = A )

Syntax hints:   -> wi 4   = wceq 1444   e. wcel 1887  (class class class)co 6290   CCcc 9537   1c1 9540   x. cmul 9544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-resscn 9596  ax-1cn 9597  ax-icn 9598  ax-addcl 9599  ax-mulcl 9601  ax-mulcom 9603  ax-mulass 9605  ax-distr 9606  ax-1rid 9609  ax-cnre 9612

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-iota 5546  df-fv 5590  df-ov 6293

This theorem is referenced by:  muladd11  9803  divrec  10286  diveq1  10301  conjmul  10324  divelunit  11774  modid  12121  expadd  12314  leexp2r  12330  nnlesq  12378  faclbnd  12475  faclbnd2  12476  faclbnd4lem3  12480  faclbnd6  12484  facavg  12486  bcn0  12495  bcn1  12498  hashf1lem2  12619  hashfac  12621  reccn2  13660  iseraltlem2  13749  iseraltlem3  13750  binom11  13890  harmonic  13917  arisum2  13919  trireciplem  13920  geoserg  13924  cvgrat  13939  fprodsplit  14020  fprodle  14050  fsumcube  14113  efzval  14156  tanhlt1  14214  tanaddlem  14220  tanadd  14221  cos01gt0  14245  absef  14251  1dvds  14317  3dvds  14369  bitsfzo  14409  bitsmod  14410  gcdmultiple  14518  sqgcd  14526  lcm1  14575  coprmdvds  14659  qredeu  14664  phiprmpw  14724  coprimeprodsq  14759  pc2dvds  14828  sumhash  14841  fldivp1  14842  pcfaclem  14843  prmpwdvds  14848  prmreclem1  14860  vdwlem3  14933  vdwlem9  14939  prmop1  14996  sylow2a  17271  odadd  17488  zsssubrg  19026  zringcyg  19060  prmirredlem  19064  mulgrhm2  19070  znrrg  19136  icopnfcnv  21970  icopnfhmeo  21971  lebnumii  21997  reparphti  22028  itg2const  22698  itg2monolem3  22710  bddibl  22797  dveflem  22931  mvth  22944  dvlipcn  22946  dvivthlem1  22960  dvfsumle  22973  dvfsumabs  22975  dvfsumlem2  22979  plyconst  23160  plyeq0lem  23164  plyco  23195  0dgrb  23200  coefv0  23202  vieta1  23265  aaliou3lem2  23299  tayl0  23317  taylply2  23323  dvtaylp  23325  taylthlem2  23329  radcnvlem1  23368  abelthlem1  23386  abelthlem2  23387  abelthlem3  23388  abelthlem7  23393  abelthlem8  23394  abelthlem9  23395  efper  23434  tangtx  23460  eflogeq  23551  logdivlti  23569  logcnlem4  23590  advlogexp  23600  cxpmul2  23634  dvcxp2  23681  cxpaddle  23692  cxpeq  23697  loglesqrt  23698  relogbexp  23717  ang180lem5  23742  isosctrlem2  23748  isosctrlem3  23749  heron  23764  2efiatan  23844  dvatan  23861  leibpi  23868  birthdaylem3  23879  jensenlem2  23913  logdiflbnd  23920  harmonicbnd4  23936  lgamgulmlem2  23955  lgamcvg2  23980  wilthlem2  23994  ftalem5  24001  ftalem5OLD  24003  basellem2  24008  basellem5  24011  basellem8  24014  0sgm  24071  muinv  24122  chpub  24148  logfaclbnd  24150  logexprlim  24153  dchrsum2  24196  sumdchr2  24198  bposlem1  24212  bposlem2  24213  bposlem5  24216  lgsquad2lem1  24286  lgsquad3  24289  2sqlem6  24297  2sqlem8  24300  chtppilim  24313  vmadivsum  24320  dchrisumlem1  24327  dchrisum0flblem1  24346  rpvmasum2  24350  dchrisum0re  24351  dchrisum0lem2a  24355  dchrisum0lem3  24357  rpvmasum  24364  mudivsum  24368  mulogsumlem  24369  vmalogdivsum2  24376  pntrsumo1  24403  pntrlog2bndlem2  24416  pntrlog2bndlem4  24418  pntrlog2bndlem5  24419  pntibndlem2  24429  pntlemc  24433  pntlemf  24443  ostth2lem2  24472  ostth2lem3  24473  ostth2lem4  24474  ostth2  24475  ostth3  24476  ttgcontlem1  24915  axpaschlem  24970  axcontlem2  24995  axcontlem4  24997  axcontlem8  25001  nmoub3i  26414  ubthlem2  26513  htthlem  26570  nmcexi  27679  nmopcoadji  27754  branmfn  27758  rearchi  28605  madjusmdetlem4  28656  ccatmulgnn0dir  29428  ofcccat  29430  subfacval2  29910  cvmliftlem2  30009  snmlff  30052  sinccvglem  30316  muls1d  30368  bcprod  30374  faclimlem1  30379  faclimlem2  30380  faclim2  30384  poimirlem29  31969  poimirlem30  31970  poimirlem31  31971  poimirlem32  31972  itg2addnclem  31993  areacirclem1  32032  areacirclem4  32035  cntotbnd  32128  irrapxlem1  35666  irrapxlem4  35669  pell1qrgaplem  35719  reglogexpbas  35745  rmspecsqrtnq  35754  rmspecfund  35757  rmxy1  35770  rmxp1  35780  rmyp1  35781  rmxm1  35782  jm2.17a  35810  jm2.18  35843  jm2.23  35851  jm2.25  35854  jm2.16nn0  35859  relexpmulnn  36301  int-mul11d  36629  nzprmdif  36668  expgrowthi  36682  expgrowth  36684  binomcxplemdvbinom  36702  binomcxplemnotnn0  36705  fmul01  37658  fmul01lt1lem1  37662  m1expevenOLD  37670  0ellimcdiv  37730  dvxpaek  37815  dvnxpaek  37817  itgiccshift  37857  itgperiod  37858  itgsbtaddcnst  37859  stoweidlem11  37871  stoweidlem26  37886  stoweidlem38  37899  wallispilem4  37930  stirlinglem1  37936  stirlinglem3  37938  stirlinglem6  37941  stirlinglem7  37942  stirlinglem8  37943  stirlinglem10  37945  stirlinglem12  37947  dirkertrigeqlem3  37962  dirkertrigeq  37963  dirkercncflem1  37965  dirkercncflem2  37966  fourierdlem28  37997  fourierdlem30  37999  fourierdlem39  38009  fourierdlem47  38017  fourierdlem60  38030  fourierdlem61  38031  fourierdlem73  38043  fourierdlem83  38053  fourierdlem87  38057  etransclem14  38113  etransclem24  38123  etransclem25  38124  etransclem35  38134  logblt1b  40428  nn0sumshdiglem2  40486