Theorem mulid1d 9613

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

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767  (class class class)co 6284   CCcc 9490   1c1 9493   x. cmul 9497

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-mulcl 9554  ax-mulcom 9556  ax-mulass 9558  ax-distr 9559  ax-1rid 9562  ax-cnre 9565

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5551  df-fv 5596  df-ov 6287

This theorem is referenced by:  muladd11  9749  divrec  10223  diveq1  10238  conjmul  10261  divelunit  11662  modid  11988  expadd  12176  leexp2r  12191  nnlesq  12239  faclbnd  12336  faclbnd2  12337  faclbnd4lem3  12341  faclbnd6  12345  facavg  12347  bcn0  12356  bcn1  12359  hashf1lem2  12471  hashfac  12473  reccn2  13382  iseraltlem2  13468  iseraltlem3  13469  binom11  13607  harmonic  13633  arisum2  13635  trireciplem  13636  geoserg  13640  cvgrat  13655  efzval  13698  tanhlt1  13756  tanaddlem  13762  tanadd  13763  cos01gt0  13787  absef  13793  1dvds  13859  3dvds  13909  bitsfzo  13944  bitsmod  13945  gcdmultiple  14047  sqgcd  14055  coprmdvds  14102  qredeu  14107  phiprmpw  14165  coprimeprodsq  14192  pc2dvds  14261  sumhash  14274  fldivp1  14275  pcfaclem  14276  prmpwdvds  14281  prmreclem1  14293  vdwlem3  14360  vdwlem9  14366  sylow2a  16445  odadd  16659  zsssubrg  18272  zringcyg  18308  zcyg  18313  prmirredlem  18318  prmirredlemOLD  18321  mulgrhm2  18328  mulgrhm2OLD  18331  znrrg  18399  icopnfcnv  21205  icopnfhmeo  21206  lebnumii  21229  reparphti  21260  itg2const  21910  itg2monolem3  21922  bddibl  22009  dveflem  22143  mvth  22156  dvlipcn  22158  dvivthlem1  22172  dvfsumle  22185  dvfsumabs  22187  dvfsumlem2  22191  plyconst  22366  plyeq0lem  22370  plyco  22401  0dgrb  22406  coefv0  22407  vieta1  22470  aaliou3lem2  22501  tayl0  22519  taylply2  22525  dvtaylp  22527  taylthlem2  22531  radcnvlem1  22570  abelthlem1  22588  abelthlem2  22589  abelthlem3  22590  abelthlem7  22595  abelthlem8  22596  abelthlem9  22597  efper  22633  tangtx  22659  eflogeq  22742  logdivlti  22761  logcnlem4  22782  advlogexp  22792  cxpmul2  22826  dvcxp2  22873  cxpaddle  22882  cxpeq  22887  loglesqrt  22888  ang180lem5  22901  isosctrlem2  22909  isosctrlem3  22910  heron  22925  2efiatan  23005  dvatan  23022  leibpi  23029  birthdaylem3  23039  jensenlem2  23073  logdiflbnd  23080  harmonicbnd4  23096  wilthlem2  23099  ftalem5  23106  basellem2  23111  basellem5  23114  basellem8  23117  0sgm  23174  muinv  23225  chpub  23251  logfaclbnd  23253  logexprlim  23256  dchrsum2  23299  sumdchr2  23301  bposlem1  23315  bposlem2  23316  bposlem5  23319  lgsquad2lem1  23389  lgsquad3  23392  2sqlem6  23400  2sqlem8  23403  chtppilim  23416  vmadivsum  23423  dchrisumlem1  23430  dchrisum0flblem1  23449  rpvmasum2  23453  dchrisum0re  23454  dchrisum0lem2a  23458  dchrisum0lem3  23460  rpvmasum  23467  mudivsum  23471  mulogsumlem  23472  vmalogdivsum2  23479  pntrsumo1  23506  pntrlog2bndlem2  23519  pntrlog2bndlem4  23521  pntrlog2bndlem5  23522  pntibndlem2  23532  pntlemc  23536  pntlemf  23546  ostth2lem2  23575  ostth2lem3  23576  ostth2lem4  23577  ostth2  23578  ostth3  23579  ttgcontlem1  23892  axpaschlem  23947  axcontlem2  23972  axcontlem4  23974  axcontlem8  23978  nmoub3i  25392  ubthlem2  25491  htthlem  25538  nmcexi  26649  nmopcoadji  26724  branmfn  26728  rearchi  27523  ccatmulgnn0dir  28164  ofcccat  28166  lgamgulmlem2  28240  lgamcvg2  28265  subfacval2  28299  cvmliftlem2  28399  snmlff  28442  sinccvglem  28541  muls1d  28624  fprodsplit  28700  faclimlem1  28773  faclimlem2  28774  faclim2  28778  fsumcube  29427  itg2addnclem  29671  areacirclem1  29712  areacirclem4  29715  cntotbnd  29923  irrapxlem1  30390  irrapxlem4  30393  pell1qrgaplem  30441  reglogexpbas  30465  rmspecsqrtnq  30474  rmspecfund  30477  rmxy1  30490  rmxp1  30500  rmyp1  30501  rmxm1  30502  jm2.17a  30530  jm2.18  30562  jm2.23  30570  jm2.25  30573  jm2.16nn0  30578  nzprmdif  30852  expgrowthi  30866  expgrowth  30868  fmul01  31158  fmul01lt1lem1  31162  m1expeven  31169  0ellimcdiv  31219  itgiccshift  31326  itgperiod  31327  itgsbtaddcnst  31328  stoweidlem11  31339  stoweidlem26  31354  stoweidlem38  31366  wallispilem4  31396  stirlinglem1  31402  stirlinglem3  31404  stirlinglem6  31407  stirlinglem7  31408  stirlinglem8  31409  stirlinglem10  31411  stirlinglem12  31413  dirkertrigeqlem3  31428  dirkertrigeq  31429  dirkercncflem1  31431  dirkercncflem2  31432  fourierdlem28  31463  fourierdlem30  31465  fourierdlem39  31474  fourierdlem47  31482  fourierdlem60  31495  fourierdlem61  31496  fourierdlem73  31508  fourierdlem83  31518  fourierdlem87  31522