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  552  ancrd  553  anim12d  610  anim1d  612  anim2d  613  orel2  890  pm2.621  898  pm2.63  940  orim1d  965  orim2d  966  ecase2dOLD  1030  cad0  1620  cad0OLD  1621  merco2  1739  exgen  1979  spnfw  1984  r19.29vva  3214  ab0w  4374  rmosn  4724  opthpr  4853  opthprneg  4866  wereu2  5674  relop  5851  frpomin  6342  fpropnf1  7266  soxp  8115  omopth2  8584  swoord2  8735  mapdom2  9148  en3lplem2  9608  rankxplim3  9876  cfsmolem  10265  fin1a2s  10409  fpwwe2lem11  10636  fpwwe2lem12  10637  inawina  10685  gchina  10694  elnnz  12568  xmullem  13243  icossicc  13413  iocssicc  13414  ioossico  13415  ioopnfsup  13829  icopnfsup  13830  expeq0  14058  repswswrd  14734  repswcshw  14762  coprmprod  16598  vdwlem6  16919  lublecllem  18313  tsrlemax  18539  ablsimpnosubgd  19974  ocv2ss  21226  issubassa3  21420  0top  22486  neindisj2  22627  lmconst  22765  cnpresti  22792  sslm  22803  cmpfi  22912  dfconn2  22923  hausflim  23485  bndth  24474  nmoleub2a  24633  nmoleub2b  24634  cmetcaulem  24805  ioorf  25090  ioorinv2  25092  dgrcolem2  25788  plydiveu  25811  dvloglem  26156  lmieu  28035  axcontlem4  28225  clwwlknwwlksn  29291  numclwwlk1lem2foa  29607  dipsubdir  30101  omssubadd  33299  subgrpth  34125  idinside  35056  endofsegid  35057  gg-dvfsumlem2  35183  nn0prpwlem  35207  meran1  35296  onsuct0  35326  bj-sngltag  35864  poimirlem26  36514  ftc1anclem7  36567  fdc1  36614  rngosubdi  36813  rngosubdir  36814  mpobi123f  37030  lkreqN  38040  cdlemg33a  39577  mapdordlem2  40508  onsucf1olem  42020  cnvtrucl0  42375  ntrneiiso  42842  3ornot23  43270  rspsbc2  43295  sbcim2g  43299  idn2  43374  idn3  43376  trsspwALT2  43580  sspwtrALT  43583  sstrALT2  43596  r19.36vf  43825  ioossioc  44205  ioossioobi  44230  stoweidlem27  44743  stoweidlem31  44747  stoweidlem60  44776  hoidmvlelem3  45313  atbiffatnnb  45622  cfsetsnfsetf1  45769  el1fzopredsuc  46033  poprelb  46192  upwlkwlk  46517  line2y  47441  elsetrecslem  47744