Theorem mulid1d 9611

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

Syntax hints:   -> wi 4   = wceq 1381   e. wcel 1802  (class class class)co 6277   CCcc 9488   1c1 9491   x. cmul 9495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-mulcl 9552  ax-mulcom 9554  ax-mulass 9556  ax-distr 9557  ax-1rid 9560  ax-cnre 9563

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-iota 5537  df-fv 5582  df-ov 6280

This theorem is referenced by:  muladd11  9748  divrec  10224  diveq1  10239  conjmul  10262  divelunit  11666  modid  11994  expadd  12182  leexp2r  12197  nnlesq  12245  faclbnd  12342  faclbnd2  12343  faclbnd4lem3  12347  faclbnd6  12351  facavg  12353  bcn0  12362  bcn1  12365  hashf1lem2  12479  hashfac  12481  reccn2  13393  iseraltlem2  13479  iseraltlem3  13480  binom11  13618  harmonic  13644  arisum2  13646  trireciplem  13647  geoserg  13651  cvgrat  13666  efzval  13709  tanhlt1  13767  tanaddlem  13773  tanadd  13774  cos01gt0  13798  absef  13804  1dvds  13870  3dvds  13922  bitsfzo  13957  bitsmod  13958  gcdmultiple  14060  sqgcd  14068  coprmdvds  14115  qredeu  14120  phiprmpw  14178  coprimeprodsq  14205  pc2dvds  14274  sumhash  14287  fldivp1  14288  pcfaclem  14289  prmpwdvds  14294  prmreclem1  14306  vdwlem3  14373  vdwlem9  14379  sylow2a  16508  odadd  16725  zsssubrg  18344  zringcyg  18380  zcyg  18385  prmirredlem  18390  prmirredlemOLD  18393  mulgrhm2  18400  mulgrhm2OLD  18403  znrrg  18471  icopnfcnv  21308  icopnfhmeo  21309  lebnumii  21332  reparphti  21363  itg2const  22013  itg2monolem3  22025  bddibl  22112  dveflem  22246  mvth  22259  dvlipcn  22261  dvivthlem1  22275  dvfsumle  22288  dvfsumabs  22290  dvfsumlem2  22294  plyconst  22469  plyeq0lem  22473  plyco  22504  0dgrb  22509  coefv0  22510  vieta1  22573  aaliou3lem2  22604  tayl0  22622  taylply2  22628  dvtaylp  22630  taylthlem2  22634  radcnvlem1  22673  abelthlem1  22691  abelthlem2  22692  abelthlem3  22693  abelthlem7  22698  abelthlem8  22699  abelthlem9  22700  efper  22737  tangtx  22763  eflogeq  22851  logdivlti  22870  logcnlem4  22891  advlogexp  22901  cxpmul2  22935  dvcxp2  22982  cxpaddle  22991  cxpeq  22996  loglesqrt  22997  ang180lem5  23010  isosctrlem2  23018  isosctrlem3  23019  heron  23034  2efiatan  23114  dvatan  23131  leibpi  23138  birthdaylem3  23148  jensenlem2  23182  logdiflbnd  23189  harmonicbnd4  23205  wilthlem2  23208  ftalem5  23215  basellem2  23220  basellem5  23223  basellem8  23226  0sgm  23283  muinv  23334  chpub  23360  logfaclbnd  23362  logexprlim  23365  dchrsum2  23408  sumdchr2  23410  bposlem1  23424  bposlem2  23425  bposlem5  23428  lgsquad2lem1  23498  lgsquad3  23501  2sqlem6  23509  2sqlem8  23512  chtppilim  23525  vmadivsum  23532  dchrisumlem1  23539  dchrisum0flblem1  23558  rpvmasum2  23562  dchrisum0re  23563  dchrisum0lem2a  23567  dchrisum0lem3  23569  rpvmasum  23576  mudivsum  23580  mulogsumlem  23581  vmalogdivsum2  23588  pntrsumo1  23615  pntrlog2bndlem2  23628  pntrlog2bndlem4  23630  pntrlog2bndlem5  23631  pntibndlem2  23641  pntlemc  23645  pntlemf  23655  ostth2lem2  23684  ostth2lem3  23685  ostth2lem4  23686  ostth2  23687  ostth3  23688  ttgcontlem1  24053  axpaschlem  24108  axcontlem2  24133  axcontlem4  24135  axcontlem8  24139  nmoub3i  25553  ubthlem2  25652  htthlem  25699  nmcexi  26810  nmopcoadji  26885  branmfn  26889  rearchi  27698  ccatmulgnn0dir  28362  ofcccat  28364  lgamgulmlem2  28438  lgamcvg2  28463  subfacval2  28497  cvmliftlem2  28597  snmlff  28640  sinccvglem  28904  muls1d  28987  fprodsplit  29063  faclimlem1  29136  faclimlem2  29137  faclim2  29141  fsumcube  29790  itg2addnclem  30034  areacirclem1  30075  areacirclem4  30078  cntotbnd  30260  irrapxlem1  30726  irrapxlem4  30729  pell1qrgaplem  30777  reglogexpbas  30801  rmspecsqrtnq  30810  rmspecfund  30813  rmxy1  30826  rmxp1  30836  rmyp1  30837  rmxm1  30838  jm2.17a  30866  jm2.18  30898  jm2.23  30906  jm2.25  30909  jm2.16nn0  30914  nzprmdif  31193  expgrowthi  31207  expgrowth  31209  fmul01  31498  fmul01lt1lem1  31502  m1expeven  31509  0ellimcdiv  31559  itgiccshift  31665  itgperiod  31666  itgsbtaddcnst  31667  stoweidlem11  31678  stoweidlem26  31693  stoweidlem38  31705  wallispilem4  31735  stirlinglem1  31741  stirlinglem3  31743  stirlinglem6  31746  stirlinglem7  31747  stirlinglem8  31748  stirlinglem10  31750  stirlinglem12  31752  dirkertrigeqlem3  31767  dirkertrigeq  31768  dirkercncflem1  31770  dirkercncflem2  31771  fourierdlem28  31802  fourierdlem30  31804  fourierdlem39  31813  fourierdlem47  31821  fourierdlem60  31834  fourierdlem61  31835  fourierdlem73  31847  fourierdlem83  31857  fourierdlem87  31861