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  891  pm2.621  899  pm2.63  943  orim1d  968  orim2d  969  cad0  1618  merco2  1736  exgen  1974  spnfw  1979  r19.29vva  3216  ab0w  4379  rmosn  4719  opthpr  4851  opthprneg  4865  wereu2  5682  relop  5861  frpomin  6361  fpropnf1  7287  soxp  8154  omopth2  8622  swoord2  8778  mapdom2  9188  en3lplem2  9653  rankxplim3  9921  cfsmolem  10310  fin1a2s  10454  fpwwe2lem11  10681  fpwwe2lem12  10682  inawina  10730  gchina  10739  elnnz  12623  xmullem  13306  icossicc  13476  iocssicc  13477  ioossico  13478  ioopnfsup  13904  icopnfsup  13905  expeq0  14133  repswswrd  14822  repswcshw  14850  coprmprod  16698  vdwlem6  17024  lublecllem  18405  tsrlemax  18631  ablsimpnosubgd  20124  ocv2ss  21691  issubassa3  21886  0top  22990  neindisj2  23131  lmconst  23269  cnpresti  23296  sslm  23307  cmpfi  23416  dfconn2  23427  hausflim  23989  bndth  24990  nmoleub2a  25150  nmoleub2b  25151  cmetcaulem  25322  ioorf  25608  ioorinv2  25610  dvfsumlem2  26067  dgrcolem2  26314  plydiveu  26340  taylthlem2  26416  dvloglem  26690  elnnzs  28387  expsne0  28414  lmieu  28792  axcontlem4  28982  clwwlknwwlksn  30057  numclwwlk1lem2foa  30373  dipsubdir  30867  omssubadd  34302  subgrpth  35139  idinside  36085  endofsegid  36086  nn0prpwlem  36323  meran1  36412  onsuct0  36442  weiunso  36467  bj-sngltag  36984  poimirlem26  37653  ftc1anclem7  37706  fdc1  37753  rngosubdi  37952  rngosubdir  37953  mpobi123f  38169  lkreqN  39171  cdlemg33a  40708  mapdordlem2  41639  fimgmcyc  42544  onsucf1olem  43283  cnvtrucl0  43637  ntrneiiso  44104  3ornot23  44529  rspsbc2  44554  sbcim2g  44558  idn2  44633  idn3  44635  trsspwALT2  44839  sspwtrALT  44842  sstrALT2  44855  r19.36vf  45141  ioossioc  45505  ioossioobi  45530  stoweidlem27  46042  stoweidlem31  46046  stoweidlem60  46075  hoidmvlelem3  46612  atbiffatnnb  46924  cfsetsnfsetf1  47071  el1fzopredsuc  47337  poprelb  47511  isubgr3stgrlem4  47936  upwlkwlk  48055  line2y  48676  elsetrecslem  49218