Theorem idd 25

Description: Principle of identity id 23 with antecedent. (Contributed by NM, 26-Nov-1995.)

Assertion

Ref	Expression
idd	⊢ (𝜑 → (𝜓 → 𝜓))

Proof of Theorem idd

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	a1i 11	1 ⊢ (𝜑 → (𝜓 → 𝜓))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1d  83  simprim  167  pm2.6  193  pm2.65  195  ancld  560  ancrd  561  anim12d  621  anim1d  623  anim2d  624  orel2  904  pm2.621  912  pm2.63  955  orim1d  981  orim2d  982  cad0  1651  merco2  1769  exgen  2007  spnfw  2012  r19.29vva  3228  rmosn  4690  opthpr  4821  opthprneg  4835  wereu2  5663  relop  5841  frpomin  6348  fpropnf1  7272  soxp  8134  omopth2  8578  swoord2  8737  mapdom2  9146  en3lplem2  9592  rankxplim3  9863  cfsmolem  10272  fin1a2s  10416  fpwwe2lem11  10644  fpwwe2lem12  10645  inawina  10693  gchina  10702  elnnz  12619  xmullem  13308  icossicc  13481  iocssicc  13482  ioossico  13483  ioopnfsup  13917  icopnfsup  13918  expeq0  14148  repswswrd  14847  repswcshw  14875  coprmprod  16744  vdwlem6  17071  lublecllem  18439  tsrlemax  18667  chnccat  18707  ablsimpnosubgd  20207  ocv2ss  21860  issubassa3  22053  0top  23177  neindisj2  23317  lmconst  23455  cnpresti  23482  sslm  23493  cmpfi  23602  dfconn2  23613  hausflim  24175  bndth  25154  nmoleub2a  25313  nmoleub2b  25314  cmetcaulem  25484  ioorf  25769  ioorinv2  25771  dvfsumlem2  26223  dgrcolem2  26468  plydiveu  26496  taylthlem2  26574  dvloglem  26850  elnnzs  28631  expsne0  28666  bdayfinbndlem1  28697  lmieu  29130  axcontlem4  29354  clwwlknwwlksn  30426  numclwwlk1lem2foa  30742  dipsubdir  31237  omssubadd  34722  subgrpth  35647  idinside  36597  endofsegid  36598  nn0prpwlem  36874  meran1  36963  onsuct0  36993  weiunso  37018  bj-axdd2ALT  37283  bj-sngltag  37660  poimirlem26  38338  ftc1anclem7  38391  fdc1  38438  rngosubdi  38637  rngosubdir  38638  mpobi123f  38852  lkreqN  39985  cdlemg33a  41521  mapdordlem2  42452  fimgmcyc  43343  onsucf1olem  44038  cnvtrucl0  44391  ntrneiiso  44858  3ornot23  45259  rspsbc2  45284  sbcim2g  45288  idn2  45363  idn3  45365  trsspwALT2  45568  sspwtrALT  45571  sstrALT2  45584  r19.36vf  45895  ioossioc  46249  ioossioobi  46274  stoweidlem27  46782  stoweidlem31  46786  stoweidlem60  46815  hoidmvlelem3  47352  chnerlem3  47641  atbiffatnnb  47690  cfsetsnfsetf1  47837  el1fzopredsuc  48104  poprelb  48314  isubgr3stgrlem4  48775  upwlkwlk  48945  line2y  49576  elsetrecslem  50518