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  4372  rmosn  4722  opthpr  4851  opthprneg  4864  wereu2  5672  relop  5848  frpomin  6338  fpropnf1  7261  soxp  8110  omopth2  8580  swoord2  8731  mapdom2  9144  en3lplem2  9604  rankxplim3  9872  cfsmolem  10261  fin1a2s  10405  fpwwe2lem11  10632  fpwwe2lem12  10633  inawina  10681  gchina  10690  elnnz  12564  xmullem  13239  icossicc  13409  iocssicc  13410  ioossico  13411  ioopnfsup  13825  icopnfsup  13826  expeq0  14054  repswswrd  14730  repswcshw  14758  coprmprod  16594  vdwlem6  16915  lublecllem  18309  tsrlemax  18535  ablsimpnosubgd  19966  ocv2ss  21210  issubassa3  21404  0top  22468  neindisj2  22609  lmconst  22747  cnpresti  22774  sslm  22785  cmpfi  22894  dfconn2  22905  hausflim  23467  bndth  24456  nmoleub2a  24615  nmoleub2b  24616  cmetcaulem  24787  ioorf  25072  ioorinv2  25074  dgrcolem2  25770  plydiveu  25793  dvloglem  26138  lmieu  28015  axcontlem4  28205  clwwlknwwlksn  29271  numclwwlk1lem2foa  29587  dipsubdir  30079  omssubadd  33237  subgrpth  34063  idinside  34994  endofsegid  34995  gg-dvfsumlem2  35121  nn0prpwlem  35145  meran1  35234  onsuct0  35264  bj-sngltag  35802  poimirlem26  36452  ftc1anclem7  36505  fdc1  36552  rngosubdi  36751  rngosubdir  36752  mpobi123f  36968  lkreqN  37978  cdlemg33a  39515  mapdordlem2  40446  onsucf1olem  41953  cnvtrucl0  42308  ntrneiiso  42775  3ornot23  43203  rspsbc2  43228  sbcim2g  43232  idn2  43307  idn3  43309  trsspwALT2  43513  sspwtrALT  43516  sstrALT2  43529  r19.36vf  43758  ioossioc  44140  ioossioobi  44165  stoweidlem27  44678  stoweidlem31  44682  stoweidlem60  44711  hoidmvlelem3  45248  atbiffatnnb  45557  cfsetsnfsetf1  45704  el1fzopredsuc  45968  poprelb  46127  upwlkwlk  46452  line2y  47343  elsetrecslem  47646