Theorem idd 24

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

Assertion

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

Proof of Theorem idd

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

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  imim1d  80  simprim  161  pm2.6  181  pm2.65  183  orel2  397  pm2.621  423  simpr  476  ancld  574  ancrd  575  anim12d  584  anim1d  586  anim2d  587  pm2.63  825  orim1d  880  orim2d  881  ecase2d  978  cad0  1547  merco2  1652  spnfw  1915  eqsbc3rOLD  3460  opthpr  4324  wereu2  5035  relop  5194  soxp  7177  omopth2  7551  swoord2  7661  mapdom2  8016  en3lplem2  8395  rankxplim3  8627  cfsmolem  8975  fin1a2s  9119  fpwwe2lem12  9342  fpwwe2lem13  9343  inawina  9391  gchina  9400  elnnz  11264  xmullem  11966  icossicc  12131  iocssicc  12132  ioossico  12133  ioopnfsup  12525  icopnfsup  12526  expeq0  12752  repswswrd  13382  repswcshw  13409  coprmprod  15213  vdwlem6  15528  lublecllem  16811  tsrlemax  17043  ocv2ss  19836  0top  20598  neindisj2  20737  lmconst  20875  cnpresti  20902  sslm  20913  cmpfi  21021  dfcon2  21032  hausflim  21595  bndth  22565  nmoleub2a  22725  nmoleub2b  22726  cmetcaulem  22894  ioorf  23147  ioorinv2  23149  dgrcolem2  23834  plydiveu  23857  dvloglem  24194  lmieu  25476  axcontlem4  25647  dipsubdir  27087  omssubadd  29689  idinside  31361  endofsegid  31362  nn0prpwlem  31487  nn0prpw  31488  meran1  31580  onsuct0  31610  bj-sngltag  32164  poimirlem26  32605  ftc1anclem7  32661  fdc1  32712  rngosubdi  32914  rngosubdir  32915  mpt2bi123f  33141  lkreqN  33475  cdlemg33a  35012  mapdordlem2  35944  cnvtrucl0  36950  ntrneiiso  37409  3ornot23  37736  rspsbc2  37765  sbcim2g  37769  idn2  37859  idn3  37861  trsspwALT2  38068  sspwtrALT  38071  sstrALT2  38092  ioossioc  38560  ioossioobi  38590  stoweidlem27  38920  stoweidlem31  38924  stoweidlem60  38953  hoidmvlelem3  39487  atbiffatnnb  39728  el1fzopredsuc  39948  fpropnf1  40337  wlk1wlk  40846  elsetrecslem  42243