Theorem mulid1d 9391

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

Syntax hints:   -> wi 4   = wceq 1362   e. wcel 1755  (class class class)co 6080   CCcc 9268   1c1 9271   x. cmul 9275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-mulcl 9332  ax-mulcom 9334  ax-mulass 9336  ax-distr 9337  ax-1rid 9340  ax-cnre 9343

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083

This theorem is referenced by:  muladd11  9527  divrec  9998  diveq1  10013  conjmul  10036  divelunit  11414  modid  11716  expadd  11890  leexp2r  11905  nnlesq  11953  faclbnd  12050  faclbnd2  12051  faclbnd4lem3  12055  faclbnd6  12059  facavg  12061  bcn0  12070  bcn1  12073  hashf1lem2  12193  hashfac  12195  reccn2  13058  iseraltlem2  13144  iseraltlem3  13145  binom11  13278  harmonic  13304  arisum2  13306  trireciplem  13307  geoserg  13311  cvgrat  13326  efzval  13369  tanhlt1  13427  tanaddlem  13433  tanadd  13434  cos01gt0  13458  absef  13464  1dvds  13530  3dvds  13579  bitsfzo  13614  bitsmod  13615  gcdmultiple  13717  sqgcd  13725  coprmdvds  13771  qredeu  13776  phiprmpw  13834  coprimeprodsq  13859  pc2dvds  13928  sumhash  13941  fldivp1  13942  pcfaclem  13943  prmpwdvds  13948  prmreclem1  13960  vdwlem3  14027  vdwlem9  14033  sylow2a  16098  odadd  16312  zsssubrg  17715  zringcyg  17749  zcyg  17754  prmirredlem  17759  prmirredlemOLD  17762  mulgrhm2  17769  mulgrhm2OLD  17772  znrrg  17840  icopnfcnv  20356  icopnfhmeo  20357  lebnumii  20380  reparphti  20411  itg2const  21060  itg2monolem3  21072  bddibl  21159  dveflem  21293  mvth  21306  dvlipcn  21308  dvivthlem1  21322  dvfsumle  21335  dvfsumabs  21337  dvfsumlem2  21341  plyconst  21559  plyeq0lem  21563  plyco  21594  0dgrb  21599  coefv0  21600  vieta1  21663  aaliou3lem2  21694  tayl0  21712  taylply2  21718  dvtaylp  21720  taylthlem2  21724  radcnvlem1  21763  abelthlem1  21781  abelthlem2  21782  abelthlem3  21783  abelthlem7  21788  abelthlem8  21789  abelthlem9  21790  efper  21826  tangtx  21852  eflogeq  21935  logdivlti  21954  logcnlem4  21975  advlogexp  21985  cxpmul2  22019  dvcxp2  22066  cxpaddle  22075  cxpeq  22080  loglesqr  22081  ang180lem5  22094  isosctrlem2  22102  isosctrlem3  22103  heron  22118  2efiatan  22198  dvatan  22215  leibpi  22222  birthdaylem3  22232  jensenlem2  22266  logdiflbnd  22273  harmonicbnd4  22289  wilthlem2  22292  ftalem5  22299  basellem2  22304  basellem5  22307  basellem8  22310  0sgm  22367  muinv  22418  chpub  22444  logfaclbnd  22446  logexprlim  22449  dchrsum2  22492  sumdchr2  22494  bposlem1  22508  bposlem2  22509  bposlem5  22512  lgsquad2lem1  22582  lgsquad3  22585  2sqlem6  22593  2sqlem8  22596  chtppilim  22609  vmadivsum  22616  dchrisumlem1  22623  dchrisum0flblem1  22642  rpvmasum2  22646  dchrisum0re  22647  dchrisum0lem2a  22651  dchrisum0lem3  22653  rpvmasum  22660  mudivsum  22664  mulogsumlem  22665  vmalogdivsum2  22672  pntrsumo1  22699  pntrlog2bndlem2  22712  pntrlog2bndlem4  22714  pntrlog2bndlem5  22715  pntibndlem2  22725  pntlemc  22729  pntlemf  22739  ostth2lem2  22768  ostth2lem3  22769  ostth2lem4  22770  ostth2  22771  ostth3  22772  ttgcontlem1  22954  axpaschlem  23009  axcontlem2  23034  axcontlem4  23036  axcontlem8  23040  nmoub3i  23996  ubthlem2  24095  htthlem  24142  nmcexi  25253  nmopcoadji  25328  branmfn  25332  rearchi  26164  ccatmulgnn0dir  26788  ofcccat  26790  lgamgulmlem2  26864  lgamcvg2  26889  subfacval2  26923  cvmliftlem2  27023  snmlff  27066  sinccvglem  27164  muls1d  27247  fprodsplit  27323  faclimlem1  27396  faclimlem2  27397  faclim2  27401  fsumcube  28050  itg2addnclem  28287  areacirclem1  28328  areacirclem4  28331  cntotbnd  28539  irrapxlem1  29008  irrapxlem4  29011  pell1qrgaplem  29059  reglogexpbas  29083  rmspecsqrnq  29092  rmspecfund  29095  rmxy1  29108  rmxp1  29118  rmyp1  29119  rmxm1  29120  jm2.17a  29148  jm2.18  29182  jm2.23  29190  jm2.25  29193  jm2.16nn0  29198  expgrowthi  29452  expgrowth  29454  fmul01  29606  fmul01lt1lem1  29610  m1expeven  29618  stoweidlem11  29652  stoweidlem26  29667  stoweidlem38  29679  wallispilem4  29709  stirlinglem1  29715  stirlinglem3  29717  stirlinglem6  29720  stirlinglem7  29721  stirlinglem8  29722  stirlinglem10  29724  stirlinglem12  29726