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  3223  rmosn  4680  opthpr  4811  opthprneg  4825  wereu2  5648  relop  5828  frpomin  6336  fpropnf1  7263  soxp  8130  omopth2  8576  swoord2  8735  mapdom2  9151  en3lplem2  9598  rankxplim3  9879  cfsmolem  10329  fin1a2s  10473  fpwwe2lem11  10707  fpwwe2lem12  10708  inawina  10756  gchina  10765  elnnz  12684  xmullem  13375  icossicc  13548  iocssicc  13549  ioossico  13550  ioopnfsup  13984  icopnfsup  13985  expeq0  14215  repswswrd  14915  repswcshw  14943  coprmprod  16816  vdwlem6  17144  lublecllem  18512  tsrlemax  18740  chnccat  18780  ablsimpnosubgd  20300  ocv2ss  21959  issubassa3  22154  0top  23281  neindisj2  23421  lmconst  23559  cnpresti  23586  sslm  23597  cmpfi  23706  dfconn2  23717  hausflim  24280  bndth  25259  nmoleub2a  25418  nmoleub2b  25419  cmetcaulem  25589  ioorf  25874  ioorinv2  25876  dvfsumlem2  26327  dgrcolem2  26573  plydiveu  26601  taylthlem2  26683  dvloglem  26958  elnnzs  28769  expsne0  28804  bdayfinbndlem1  28835  lmieu  29271  axcontlem4  29527  subgrpth  30338  clwwlknwwlksn  30611  numclwwlk1lem2foa  30937  dipsubdir  31432  omssubadd  34915  idinside  36819  endofsegid  36820  nn0prpwlem  37080  meran1  37169  onsuct0  37199  weiunso  37224  bj-axdd2ALT  37489  bj-sngltag  37866  poimirlem26  38532  ftc1anclem7  38585  fdc1  38648  rngosubdi  38847  rngosubdir  38848  mpobi123f  39062  lkreqN  40195  cdlemg33a  41731  mapdordlem2  42662  fimgmcyc  43560  onsucf1olem  44230  cnvtrucl0  44583  ntrneiiso  45050  3ornot23  45451  rspsbc2  45476  sbcim2g  45480  idn2  45555  idn3  45557  trsspwALT2  45760  sspwtrALT  45763  sstrALT2  45776  r19.36vf  46094  ioossioc  46448  ioossioobi  46473  stoweidlem27  46981  stoweidlem31  46985  stoweidlem60  47014  hoidmvlelem3  47551  chnerlem3  47838  atbiffatnnb  47926  cfsetsnfsetf1  48073  el1fzopredsuc  48340  poprelb  48550  isubgr3stgrlem4  49011  upwlkwlk  49181  line2y  49811  elsetrecslem  50736