Theorem mulid1d 9395

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

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756  (class class class)co 6086   CCcc 9272   1c1 9275   x. cmul 9279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-mulcl 9336  ax-mulcom 9338  ax-mulass 9340  ax-distr 9341  ax-1rid 9344  ax-cnre 9347

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089

This theorem is referenced by:  muladd11  9531  divrec  10002  diveq1  10017  conjmul  10040  divelunit  11419  modid  11724  expadd  11898  leexp2r  11913  nnlesq  11961  faclbnd  12058  faclbnd2  12059  faclbnd4lem3  12063  faclbnd6  12067  facavg  12069  bcn0  12078  bcn1  12081  hashf1lem2  12201  hashfac  12203  reccn2  13066  iseraltlem2  13152  iseraltlem3  13153  binom11  13287  harmonic  13313  arisum2  13315  trireciplem  13316  geoserg  13320  cvgrat  13335  efzval  13378  tanhlt1  13436  tanaddlem  13442  tanadd  13443  cos01gt0  13467  absef  13473  1dvds  13539  3dvds  13588  bitsfzo  13623  bitsmod  13624  gcdmultiple  13726  sqgcd  13734  coprmdvds  13780  qredeu  13785  phiprmpw  13843  coprimeprodsq  13868  pc2dvds  13937  sumhash  13950  fldivp1  13951  pcfaclem  13952  prmpwdvds  13957  prmreclem1  13969  vdwlem3  14036  vdwlem9  14042  sylow2a  16109  odadd  16323  zsssubrg  17851  zringcyg  17887  zcyg  17892  prmirredlem  17897  prmirredlemOLD  17900  mulgrhm2  17907  mulgrhm2OLD  17910  znrrg  17978  icopnfcnv  20494  icopnfhmeo  20495  lebnumii  20518  reparphti  20549  itg2const  21198  itg2monolem3  21210  bddibl  21297  dveflem  21431  mvth  21444  dvlipcn  21446  dvivthlem1  21460  dvfsumle  21473  dvfsumabs  21475  dvfsumlem2  21479  plyconst  21654  plyeq0lem  21658  plyco  21689  0dgrb  21694  coefv0  21695  vieta1  21758  aaliou3lem2  21789  tayl0  21807  taylply2  21813  dvtaylp  21815  taylthlem2  21819  radcnvlem1  21858  abelthlem1  21876  abelthlem2  21877  abelthlem3  21878  abelthlem7  21883  abelthlem8  21884  abelthlem9  21885  efper  21921  tangtx  21947  eflogeq  22030  logdivlti  22049  logcnlem4  22070  advlogexp  22080  cxpmul2  22114  dvcxp2  22161  cxpaddle  22170  cxpeq  22175  loglesqr  22176  ang180lem5  22189  isosctrlem2  22197  isosctrlem3  22198  heron  22213  2efiatan  22293  dvatan  22310  leibpi  22317  birthdaylem3  22327  jensenlem2  22361  logdiflbnd  22368  harmonicbnd4  22384  wilthlem2  22387  ftalem5  22394  basellem2  22399  basellem5  22402  basellem8  22405  0sgm  22462  muinv  22513  chpub  22539  logfaclbnd  22541  logexprlim  22544  dchrsum2  22587  sumdchr2  22589  bposlem1  22603  bposlem2  22604  bposlem5  22607  lgsquad2lem1  22677  lgsquad3  22680  2sqlem6  22688  2sqlem8  22691  chtppilim  22704  vmadivsum  22711  dchrisumlem1  22718  dchrisum0flblem1  22737  rpvmasum2  22741  dchrisum0re  22742  dchrisum0lem2a  22746  dchrisum0lem3  22748  rpvmasum  22755  mudivsum  22759  mulogsumlem  22760  vmalogdivsum2  22767  pntrsumo1  22794  pntrlog2bndlem2  22807  pntrlog2bndlem4  22809  pntrlog2bndlem5  22810  pntibndlem2  22820  pntlemc  22824  pntlemf  22834  ostth2lem2  22863  ostth2lem3  22864  ostth2lem4  22865  ostth2  22866  ostth3  22867  ttgcontlem1  23099  axpaschlem  23154  axcontlem2  23179  axcontlem4  23181  axcontlem8  23185  nmoub3i  24141  ubthlem2  24240  htthlem  24287  nmcexi  25398  nmopcoadji  25473  branmfn  25477  rearchi  26279  ccatmulgnn0dir  26909  ofcccat  26911  lgamgulmlem2  26985  lgamcvg2  27010  subfacval2  27044  cvmliftlem2  27144  snmlff  27187  sinccvglem  27286  muls1d  27369  fprodsplit  27445  faclimlem1  27518  faclimlem2  27519  faclim2  27523  fsumcube  28172  itg2addnclem  28414  areacirclem1  28455  areacirclem4  28458  cntotbnd  28666  irrapxlem1  29134  irrapxlem4  29137  pell1qrgaplem  29185  reglogexpbas  29209  rmspecsqrnq  29218  rmspecfund  29221  rmxy1  29234  rmxp1  29244  rmyp1  29245  rmxm1  29246  jm2.17a  29274  jm2.18  29308  jm2.23  29316  jm2.25  29319  jm2.16nn0  29324  expgrowthi  29578  expgrowth  29580  fmul01  29732  fmul01lt1lem1  29736  m1expeven  29743  stoweidlem11  29777  stoweidlem26  29792  stoweidlem38  29804  wallispilem4  29834  stirlinglem1  29840  stirlinglem3  29842  stirlinglem6  29845  stirlinglem7  29846  stirlinglem8  29847  stirlinglem10  29849  stirlinglem12  29851