Theorem mulid2d 10058

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
addcld.1	|- ( ph -> A e. CC )

Assertion

Ref	Expression
mulid2d	|- ( ph -> ( 1 x. A ) = A )

Proof of Theorem mulid2d

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		mulid2 10038	. 2 |- ( A e. CC -> ( 1 x. A ) = A )
3	1, 2	syl 17	1 |- ( ph -> ( 1 x. A ) = A )

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   1c1 9937   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-mulcom 10000  ax-mulass 10002  ax-distr 10003  ax-1rid 10006  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  adddirp1d  10066  addid1  10216  mulsubfacd  10492  mulcand  10660  receu  10672  divdivdiv  10726  divcan5  10727  subrec  10854  ltrec  10905  recp1lt1  10921  nndivtr  11062  subhalfhalf  11266  xp1d2m1eqxm1d2  11286  gtndiv  11454  lincmb01cmp  12315  iccf1o  12316  ltdifltdiv  12635  modfrac  12683  negmod  12715  addmodid  12718  m1expcl2  12882  expgt1  12898  ltexp2a  12912  leexp2a  12916  binom3  12985  faclbnd  13077  faclbnd4lem4  13083  facavg  13088  bcval5  13105  cshweqrep  13567  sqrlem2  13984  absimle  14049  reccn2  14327  iseraltlem2  14413  iseraltlem3  14414  o1fsum  14545  abscvgcvg  14551  ackbijnn  14560  binom1p  14563  binom1dif  14565  incexclem  14568  incexc  14569  climcndslem1  14581  geomulcvg  14607  fprodsplit  14696  fallrisefac  14756  bpolysum  14784  bpolydiflem  14785  bpoly4  14790  efcllem  14808  ef01bndlem  14914  efieq1re  14929  eirrlem  14932  iddvds  14995  pwp1fsum  15114  oddpwp1fsum  15115  bitsfzolem  15156  bitsfzo  15157  rpmulgcd  15275  prmind2  15398  isprm5  15419  phiprm  15482  eulerthlem2  15487  fermltl  15489  hashgcdlem  15493  odzdvds  15500  powm2modprm  15508  modprm0  15510  pythagtriplem4  15524  pcexp  15564  4sqlem18  15666  vdwapun  15678  mulgnnass  17576  mulgnnassOLD  17577  odinv  17978  odadd2  18252  pgpfaclem2  18481  abvneg  18834  nrginvrcnlem  22495  nmoid  22546  blcvx  22601  icopnfcnv  22741  reparphti  22797  pcorevlem  22826  ncvsm1  22954  ncvspi  22956  cphipval2  23040  cphipval  23042  itg11  23458  itg2mulc  23514  itg2monolem1  23517  itgcnlem  23556  iblabs  23595  dvexp  23716  dvmptdiv  23737  dvef  23743  lhop1lem  23776  dvcvx  23783  dvfsumlem1  23789  dvfsumlem2  23790  dvfsumlem4  23792  dvfsum2  23797  plypow  23961  dgrcolem1  24029  vieta1lem2  24066  radcnvlem1  24167  radcnvlem2  24168  dvradcnv  24175  abelthlem2  24186  abelthlem6  24190  abelthlem7  24192  abelth2  24196  sinhalfpip  24244  sinhalfpim  24245  coshalfpip  24246  coshalfpim  24247  tangtx  24257  efif1olem4  24291  abslogle  24364  logdivlti  24366  advlog  24400  advlogexp  24401  logtayl  24406  cxpaddlelem  24492  cxpaddle  24493  affineequiv  24553  affineequiv2  24554  chordthmlem5  24563  dcubic2  24571  dcubic  24573  mcubic  24574  binom4  24577  dquartlem1  24578  quart1lem  24582  quart1  24583  quartlem1  24584  quart  24588  efiasin  24615  atantayl  24664  cvxcl  24711  scvxcvx  24712  lgamgulmlem5  24759  lgamcvg2  24781  lgam1  24790  wilthlem1  24794  wilthlem2  24795  basellem9  24815  fsumfldivdiaglem  24915  muinv  24919  chpub  24945  logexprlim  24950  mersenne  24952  perfectlem2  24955  dchrmulid2  24977  dchrptlem1  24989  dchrsum2  24993  sumdchr2  24995  bposlem2  25010  bposlem9  25017  lgsval2lem  25032  lgsval4a  25044  lgsneg1  25047  lgsdir2lem4  25053  lgsdir  25057  lgsmulsqcoprm  25068  lgsdirnn0  25069  lgsdinn0  25070  gausslemma2dlem1a  25090  gausslemma2dlem4  25094  gausslemma2dlem7  25098  gausslemma2d  25099  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem4  25103  lgsquad2lem1  25109  2sqlem8  25151  chebbnd1lem3  25160  chpchtlim  25168  rplogsumlem1  25173  rplogsumlem2  25174  rpvmasumlem  25176  dchrmusum2  25183  dchrvmasum2lem  25185  dchrvmasumlem2  25187  dchrvmasumlem3  25188  dchrisum0flblem1  25197  mulog2sumlem2  25224  vmalogdivsum2  25227  2vmadivsumlem  25229  log2sumbnd  25233  selberglem2  25235  chpdifbndlem1  25242  selberg3lem1  25246  selberg4lem1  25249  pntrlog2bndlem2  25267  pntrlog2bndlem5  25270  pntpbnd1  25275  pntpbnd2  25276  pntibndlem2  25280  pntlemb  25286  pntlemr  25291  pntlemk  25295  pntlemo  25296  brbtwn2  25785  colinearalglem4  25789  ax5seglem3  25811  axbtwnid  25819  axpaschlem  25820  axeuclidlem  25842  axcontlem7  25850  axcontlem8  25851  nvm1  27520  nvpi  27522  nvmtri  27526  ipval2  27562  ipasslem1  27686  ipasslem4  27689  bcs2  28039  lnfnaddi  28902  nnmulge  29515  sqsscirc1  29954  indsum  30083  indsumin  30084  eulerpartlemgs2  30442  plymulx0  30624  logdivsqrle  30728  subfacp1lem6  31167  subfaclim  31170  cvxpconn  31224  cvxsconn  31225  resconn  31228  sinccvglem  31566  fwddifn0  32271  nn0prpwlem  32317  knoppndvlem9  32511  knoppndvlem14  32516  bj-bary1lem1  33161  mblfinlem3  33448  itg2addnclem3  33463  iblabsnc  33474  iblmulc2nc  33475  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  areacirclem1  33500  bfplem2  33622  bfp  33623  rrntotbnd  33635  irrapxlem5  37390  pellexlem2  37394  pellexlem6  37398  pellfundex  37450  jm2.19lem3  37558  jm2.25  37566  jm2.27c  37574  jm3.1lem2  37585  flcidc  37744  int-mul12d  38486  cvgdvgrat  38512  bccn1  38543  binomcxplemnotnn0  38555  fperiodmullem  39517  xralrple2  39570  fmul01lt1lem2  39817  mccllem  39829  reclimc  39885  cosknegpi  40080  dvsinax  40127  dvnxpaek  40157  dvnmul  40158  itgsinexp  40170  stoweidlem14  40231  stoweidlem26  40243  wallispilem4  40285  wallispilem5  40286  wallispi2lem1  40288  wallispi2  40290  stirlinglem1  40291  stirlinglem3  40293  stirlinglem4  40294  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem10  40300  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkercncflem2  40321  fourierdlem26  40350  fourierdlem41  40365  fourierdlem42  40366  fourierdlem56  40379  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fourierdlem64  40387  fourierdlem65  40388  fourierdlem95  40418  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  etransclem23  40474  etransclem35  40486  etransclem46  40497  fmtnorec2lem  41454  fmtnorec3  41460  pwdif  41501  m1expoddALTV  41561  perfectALTVlem2  41631  ztprmneprm  42125  altgsumbc  42130  divge1b  42302  divgt1b  42303