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  191  pm2.65  193  ancld  550  ancrd  551  anim12d  609  anim1d  611  anim2d  612  orel2  890  pm2.621  898  pm2.63  942  orim1d  967  orim2d  968  cad0  1618  merco2  1736  exgen  1974  spnfw  1979  r19.29vva  3189  ab0w  4332  rmosn  4673  opthpr  4805  opthprneg  4819  wereu2  5620  relop  5797  frpomin  6292  fpropnf1  7208  soxp  8069  omopth2  8509  swoord2  8665  mapdom2  9072  en3lplem2  9528  rankxplim3  9796  cfsmolem  10183  fin1a2s  10327  fpwwe2lem11  10554  fpwwe2lem12  10555  inawina  10603  gchina  10612  elnnz  12499  xmullem  13184  icossicc  13357  iocssicc  13358  ioossico  13359  ioopnfsup  13786  icopnfsup  13787  expeq0  14017  repswswrd  14708  repswcshw  14736  coprmprod  16590  vdwlem6  16916  lublecllem  18282  tsrlemax  18510  ablsimpnosubgd  20003  ocv2ss  21598  issubassa3  21791  0top  22886  neindisj2  23026  lmconst  23164  cnpresti  23191  sslm  23202  cmpfi  23311  dfconn2  23322  hausflim  23884  bndth  24873  nmoleub2a  25033  nmoleub2b  25034  cmetcaulem  25204  ioorf  25490  ioorinv2  25492  dvfsumlem2  25949  dgrcolem2  26196  plydiveu  26222  taylthlem2  26298  dvloglem  26573  elnnzs  28312  expsne0  28346  lmieu  28747  axcontlem4  28930  clwwlknwwlksn  30000  numclwwlk1lem2foa  30316  dipsubdir  30810  omssubadd  34267  subgrpth  35106  idinside  36057  endofsegid  36058  nn0prpwlem  36295  meran1  36384  onsuct0  36414  weiunso  36439  bj-sngltag  36956  poimirlem26  37625  ftc1anclem7  37678  fdc1  37725  rngosubdi  37924  rngosubdir  37925  mpobi123f  38141  lkreqN  39148  cdlemg33a  40685  mapdordlem2  41616  fimgmcyc  42507  onsucf1olem  43243  cnvtrucl0  43597  ntrneiiso  44064  3ornot23  44483  rspsbc2  44508  sbcim2g  44512  idn2  44587  idn3  44589  trsspwALT2  44792  sspwtrALT  44795  sstrALT2  44808  r19.36vf  45114  ioossioc  45474  ioossioobi  45499  stoweidlem27  46009  stoweidlem31  46013  stoweidlem60  46042  hoidmvlelem3  46579  atbiffatnnb  46897  cfsetsnfsetf1  47044  el1fzopredsuc  47310  poprelb  47509  isubgr3stgrlem4  47954  upwlkwlk  48124  line2y  48741  elsetrecslem  49685