Theorem mulid1d 9513

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

Syntax hints:   -> wi 4   = wceq 1370   e. wcel 1758  (class class class)co 6199   CCcc 9390   1c1 9393   x. cmul 9397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-resscn 9449  ax-1cn 9450  ax-icn 9451  ax-addcl 9452  ax-mulcl 9454  ax-mulcom 9456  ax-mulass 9458  ax-distr 9459  ax-1rid 9462  ax-cnre 9465

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-iota 5488  df-fv 5533  df-ov 6202

This theorem is referenced by:  muladd11  9649  divrec  10120  diveq1  10135  conjmul  10158  divelunit  11543  modid  11848  expadd  12022  leexp2r  12037  nnlesq  12085  faclbnd  12182  faclbnd2  12183  faclbnd4lem3  12187  faclbnd6  12191  facavg  12193  bcn0  12202  bcn1  12205  hashf1lem2  12326  hashfac  12328  reccn2  13191  iseraltlem2  13277  iseraltlem3  13278  binom11  13412  harmonic  13438  arisum2  13440  trireciplem  13441  geoserg  13445  cvgrat  13460  efzval  13503  tanhlt1  13561  tanaddlem  13567  tanadd  13568  cos01gt0  13592  absef  13598  1dvds  13664  3dvds  13713  bitsfzo  13748  bitsmod  13749  gcdmultiple  13851  sqgcd  13859  coprmdvds  13905  qredeu  13910  phiprmpw  13968  coprimeprodsq  13993  pc2dvds  14062  sumhash  14075  fldivp1  14076  pcfaclem  14077  prmpwdvds  14082  prmreclem1  14094  vdwlem3  14161  vdwlem9  14167  sylow2a  16238  odadd  16452  zsssubrg  17995  zringcyg  18031  zcyg  18036  prmirredlem  18041  prmirredlemOLD  18044  mulgrhm2  18051  mulgrhm2OLD  18054  znrrg  18122  icopnfcnv  20645  icopnfhmeo  20646  lebnumii  20669  reparphti  20700  itg2const  21350  itg2monolem3  21362  bddibl  21449  dveflem  21583  mvth  21596  dvlipcn  21598  dvivthlem1  21612  dvfsumle  21625  dvfsumabs  21627  dvfsumlem2  21631  plyconst  21806  plyeq0lem  21810  plyco  21841  0dgrb  21846  coefv0  21847  vieta1  21910  aaliou3lem2  21941  tayl0  21959  taylply2  21965  dvtaylp  21967  taylthlem2  21971  radcnvlem1  22010  abelthlem1  22028  abelthlem2  22029  abelthlem3  22030  abelthlem7  22035  abelthlem8  22036  abelthlem9  22037  efper  22073  tangtx  22099  eflogeq  22182  logdivlti  22201  logcnlem4  22222  advlogexp  22232  cxpmul2  22266  dvcxp2  22313  cxpaddle  22322  cxpeq  22327  loglesqr  22328  ang180lem5  22341  isosctrlem2  22349  isosctrlem3  22350  heron  22365  2efiatan  22445  dvatan  22462  leibpi  22469  birthdaylem3  22479  jensenlem2  22513  logdiflbnd  22520  harmonicbnd4  22536  wilthlem2  22539  ftalem5  22546  basellem2  22551  basellem5  22554  basellem8  22557  0sgm  22614  muinv  22665  chpub  22691  logfaclbnd  22693  logexprlim  22696  dchrsum2  22739  sumdchr2  22741  bposlem1  22755  bposlem2  22756  bposlem5  22759  lgsquad2lem1  22829  lgsquad3  22832  2sqlem6  22840  2sqlem8  22843  chtppilim  22856  vmadivsum  22863  dchrisumlem1  22870  dchrisum0flblem1  22889  rpvmasum2  22893  dchrisum0re  22894  dchrisum0lem2a  22898  dchrisum0lem3  22900  rpvmasum  22907  mudivsum  22911  mulogsumlem  22912  vmalogdivsum2  22919  pntrsumo1  22946  pntrlog2bndlem2  22959  pntrlog2bndlem4  22961  pntrlog2bndlem5  22962  pntibndlem2  22972  pntlemc  22976  pntlemf  22986  ostth2lem2  23015  ostth2lem3  23016  ostth2lem4  23017  ostth2  23018  ostth3  23019  ttgcontlem1  23282  axpaschlem  23337  axcontlem2  23362  axcontlem4  23364  axcontlem8  23368  nmoub3i  24324  ubthlem2  24423  htthlem  24470  nmcexi  25581  nmopcoadji  25656  branmfn  25660  rearchi  26454  ccatmulgnn0dir  27083  ofcccat  27085  lgamgulmlem2  27159  lgamcvg2  27184  subfacval2  27218  cvmliftlem2  27318  snmlff  27361  sinccvglem  27460  muls1d  27543  fprodsplit  27619  faclimlem1  27692  faclimlem2  27693  faclim2  27697  fsumcube  28346  itg2addnclem  28590  areacirclem1  28631  areacirclem4  28634  cntotbnd  28842  irrapxlem1  29310  irrapxlem4  29313  pell1qrgaplem  29361  reglogexpbas  29385  rmspecsqrnq  29394  rmspecfund  29397  rmxy1  29410  rmxp1  29420  rmyp1  29421  rmxm1  29422  jm2.17a  29450  jm2.18  29484  jm2.23  29492  jm2.25  29495  jm2.16nn0  29500  expgrowthi  29754  expgrowth  29756  fmul01  29908  fmul01lt1lem1  29912  m1expeven  29919  stoweidlem11  29953  stoweidlem26  29968  stoweidlem38  29980  wallispilem4  30010  stirlinglem1  30016  stirlinglem3  30018  stirlinglem6  30021  stirlinglem7  30022  stirlinglem8  30023  stirlinglem10  30025  stirlinglem12  30027