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  82  simprim  166  pm2.6  190  pm2.65  192  ancld  551  ancrd  552  anim12d  609  anim1d  611  anim2d  612  orel2  888  pm2.621  896  pm2.63  938  orim1d  963  orim2d  964  ecase2dOLD  1028  cad0  1624  cad0OLD  1625  merco2  1743  exgen  1982  spnfw  1987  r19.29vva  3266  ab0w  4313  rmosn  4661  opthpr  4788  opthprneg  4801  wereu2  5586  relop  5757  frpomin  6241  fpropnf1  7135  soxp  7959  omopth2  8398  swoord2  8511  mapdom2  8915  en3lplem2  9347  rankxplim3  9638  cfsmolem  10025  fin1a2s  10169  fpwwe2lem11  10396  fpwwe2lem12  10397  inawina  10445  gchina  10454  elnnz  12327  xmullem  12995  icossicc  13165  iocssicc  13166  ioossico  13167  ioopnfsup  13580  icopnfsup  13581  expeq0  13809  repswswrd  14493  repswcshw  14521  coprmprod  16362  vdwlem6  16683  lublecllem  18074  tsrlemax  18300  ablsimpnosubgd  19703  ocv2ss  20874  issubassa3  21068  0top  22129  neindisj2  22270  lmconst  22408  cnpresti  22435  sslm  22446  cmpfi  22555  dfconn2  22566  hausflim  23128  bndth  24117  nmoleub2a  24276  nmoleub2b  24277  cmetcaulem  24448  ioorf  24733  ioorinv2  24735  dgrcolem2  25431  plydiveu  25454  dvloglem  25799  lmieu  27141  axcontlem4  27331  clwwlknwwlksn  28396  numclwwlk1lem2foa  28712  dipsubdir  29204  omssubadd  32261  subgrpth  33090  idinside  34380  endofsegid  34381  nn0prpwlem  34505  meran1  34594  onsuct0  34624  bj-sngltag  35167  poimirlem26  35797  ftc1anclem7  35850  fdc1  35898  rngosubdi  36097  rngosubdir  36098  mpobi123f  36314  lkreqN  37178  cdlemg33a  38714  mapdordlem2  39645  cnvtrucl0  41200  ntrneiiso  41669  3ornot23  42097  rspsbc2  42122  sbcim2g  42126  idn2  42201  idn3  42203  trsspwALT2  42407  sspwtrALT  42410  sstrALT2  42423  r19.36vf  42653  ioossioc  42999  ioossioobi  43024  stoweidlem27  43537  stoweidlem31  43541  stoweidlem60  43570  hoidmvlelem3  44104  atbiffatnnb  44373  cfsetsnfsetf1  44519  el1fzopredsuc  44784  poprelb  44943  upwlkwlk  45268  line2y  46068  elsetrecslem  46371