Theorem mulid1d 9602

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 1823  (class class class)co 6270   CCcc 9479   1c1 9482   x. cmul 9486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-mulcl 9543  ax-mulcom 9545  ax-mulass 9547  ax-distr 9548  ax-1rid 9551  ax-cnre 9554

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273

This theorem is referenced by:  muladd11  9739  divrec  10219  diveq1  10234  conjmul  10257  divelunit  11665  modid  12002  expadd  12190  leexp2r  12205  nnlesq  12253  faclbnd  12350  faclbnd2  12351  faclbnd4lem3  12355  faclbnd6  12359  facavg  12361  bcn0  12370  bcn1  12373  hashf1lem2  12489  hashfac  12491  reccn2  13501  iseraltlem2  13587  iseraltlem3  13588  binom11  13726  harmonic  13752  arisum2  13754  trireciplem  13755  geoserg  13759  cvgrat  13774  fprodsplit  13852  efzval  13919  tanhlt1  13977  tanaddlem  13983  tanadd  13984  cos01gt0  14008  absef  14014  1dvds  14082  3dvds  14134  bitsfzo  14169  bitsmod  14170  gcdmultiple  14272  sqgcd  14280  coprmdvds  14327  qredeu  14332  phiprmpw  14390  coprimeprodsq  14417  pc2dvds  14486  sumhash  14499  fldivp1  14500  pcfaclem  14501  prmpwdvds  14506  prmreclem1  14518  vdwlem3  14585  vdwlem9  14591  sylow2a  16838  odadd  17055  zsssubrg  18671  zringcyg  18701  prmirredlem  18705  mulgrhm2  18711  znrrg  18777  icopnfcnv  21608  icopnfhmeo  21609  lebnumii  21632  reparphti  21663  itg2const  22313  itg2monolem3  22325  bddibl  22412  dveflem  22546  mvth  22559  dvlipcn  22561  dvivthlem1  22575  dvfsumle  22588  dvfsumabs  22590  dvfsumlem2  22594  plyconst  22769  plyeq0lem  22773  plyco  22804  0dgrb  22809  coefv0  22811  vieta1  22874  aaliou3lem2  22905  tayl0  22923  taylply2  22929  dvtaylp  22931  taylthlem2  22935  radcnvlem1  22974  abelthlem1  22992  abelthlem2  22993  abelthlem3  22994  abelthlem7  22999  abelthlem8  23000  abelthlem9  23001  efper  23038  tangtx  23064  eflogeq  23155  logdivlti  23173  logcnlem4  23194  advlogexp  23204  cxpmul2  23238  dvcxp2  23285  cxpaddle  23294  cxpeq  23299  loglesqrt  23300  relogbexp  23319  ang180lem5  23344  isosctrlem2  23350  isosctrlem3  23351  heron  23366  2efiatan  23446  dvatan  23463  leibpi  23470  birthdaylem3  23481  jensenlem2  23515  logdiflbnd  23522  harmonicbnd4  23538  wilthlem2  23541  ftalem5  23548  basellem2  23553  basellem5  23556  basellem8  23559  0sgm  23616  muinv  23667  chpub  23693  logfaclbnd  23695  logexprlim  23698  dchrsum2  23741  sumdchr2  23743  bposlem1  23757  bposlem2  23758  bposlem5  23761  lgsquad2lem1  23831  lgsquad3  23834  2sqlem6  23842  2sqlem8  23845  chtppilim  23858  vmadivsum  23865  dchrisumlem1  23872  dchrisum0flblem1  23891  rpvmasum2  23895  dchrisum0re  23896  dchrisum0lem2a  23900  dchrisum0lem3  23902  rpvmasum  23909  mudivsum  23913  mulogsumlem  23914  vmalogdivsum2  23921  pntrsumo1  23948  pntrlog2bndlem2  23961  pntrlog2bndlem4  23963  pntrlog2bndlem5  23964  pntibndlem2  23974  pntlemc  23978  pntlemf  23988  ostth2lem2  24017  ostth2lem3  24018  ostth2lem4  24019  ostth2  24020  ostth3  24021  ttgcontlem1  24390  axpaschlem  24445  axcontlem2  24470  axcontlem4  24472  axcontlem8  24476  nmoub3i  25886  ubthlem2  25985  htthlem  26032  nmcexi  27143  nmopcoadji  27218  branmfn  27222  rearchi  28067  ccatmulgnn0dir  28760  ofcccat  28762  lgamgulmlem2  28836  lgamcvg2  28861  subfacval2  28895  cvmliftlem2  28995  snmlff  29038  sinccvglem  29302  muls1d  29360  faclimlem1  29409  faclimlem2  29410  faclim2  29414  fsumcube  30050  itg2addnclem  30306  areacirclem1  30347  areacirclem4  30350  cntotbnd  30532  irrapxlem1  30997  irrapxlem4  31000  pell1qrgaplem  31048  reglogexpbas  31072  rmspecsqrtnq  31081  rmspecfund  31084  rmxy1  31097  rmxp1  31107  rmyp1  31108  rmxm1  31109  jm2.17a  31137  jm2.18  31169  jm2.23  31177  jm2.25  31180  jm2.16nn0  31185  nzprmdif  31465  expgrowthi  31479  expgrowth  31481  binomcxplemdvbinom  31499  binomcxplemnotnn0  31502  fmul01  31813  fmul01lt1lem1  31817  m1expeven  31824  fprodle  31843  0ellimcdiv  31894  dvxpaek  31976  dvnxpaek  31978  itgiccshift  32018  itgperiod  32019  itgsbtaddcnst  32020  stoweidlem11  32032  stoweidlem26  32047  stoweidlem38  32059  wallispilem4  32089  stirlinglem1  32095  stirlinglem3  32097  stirlinglem6  32100  stirlinglem7  32101  stirlinglem8  32102  stirlinglem10  32104  stirlinglem12  32106  dirkertrigeqlem3  32121  dirkertrigeq  32122  dirkercncflem1  32124  dirkercncflem2  32125  fourierdlem28  32156  fourierdlem30  32158  fourierdlem39  32167  fourierdlem47  32175  fourierdlem60  32188  fourierdlem61  32189  fourierdlem73  32201  fourierdlem83  32211  fourierdlem87  32215  etransclem14  32270  etransclem24  32280  etransclem25  32281  etransclem35  32291  logblt1b  33439  nn0sumshdiglem2  33497  relexpmulnn  38227  int-mul11d  38455