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  3197  ab0w  4342  rmosn  4683  opthpr  4815  opthprneg  4829  wereu2  5635  relop  5814  frpomin  6313  fpropnf1  7242  soxp  8108  omopth2  8548  swoord2  8704  mapdom2  9112  en3lplem2  9566  rankxplim3  9834  cfsmolem  10223  fin1a2s  10367  fpwwe2lem11  10594  fpwwe2lem12  10595  inawina  10643  gchina  10652  elnnz  12539  xmullem  13224  icossicc  13397  iocssicc  13398  ioossico  13399  ioopnfsup  13826  icopnfsup  13827  expeq0  14057  repswswrd  14749  repswcshw  14777  coprmprod  16631  vdwlem6  16957  lublecllem  18319  tsrlemax  18545  ablsimpnosubgd  20036  ocv2ss  21582  issubassa3  21775  0top  22870  neindisj2  23010  lmconst  23148  cnpresti  23175  sslm  23186  cmpfi  23295  dfconn2  23306  hausflim  23868  bndth  24857  nmoleub2a  25017  nmoleub2b  25018  cmetcaulem  25188  ioorf  25474  ioorinv2  25476  dvfsumlem2  25933  dgrcolem2  26180  plydiveu  26206  taylthlem2  26282  dvloglem  26557  elnnzs  28289  expsne0  28321  lmieu  28711  axcontlem4  28894  clwwlknwwlksn  29967  numclwwlk1lem2foa  30283  dipsubdir  30777  omssubadd  34291  subgrpth  35121  idinside  36072  endofsegid  36073  nn0prpwlem  36310  meran1  36399  onsuct0  36429  weiunso  36454  bj-sngltag  36971  poimirlem26  37640  ftc1anclem7  37693  fdc1  37740  rngosubdi  37939  rngosubdir  37940  mpobi123f  38156  lkreqN  39163  cdlemg33a  40700  mapdordlem2  41631  fimgmcyc  42522  onsucf1olem  43259  cnvtrucl0  43613  ntrneiiso  44080  3ornot23  44499  rspsbc2  44524  sbcim2g  44528  idn2  44603  idn3  44605  trsspwALT2  44808  sspwtrALT  44811  sstrALT2  44824  r19.36vf  45130  ioossioc  45490  ioossioobi  45515  stoweidlem27  46025  stoweidlem31  46029  stoweidlem60  46058  hoidmvlelem3  46595  atbiffatnnb  46913  cfsetsnfsetf1  47060  el1fzopredsuc  47326  poprelb  47525  isubgr3stgrlem4  47968  upwlkwlk  48127  line2y  48744  elsetrecslem  49688