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  550  ancrd  551  anim12d  608  anim1d  610  anim2d  611  orel2  887  pm2.621  895  pm2.63  937  orim1d  962  orim2d  963  ecase2dOLD  1027  cad0  1615  cad0OLD  1616  merco2  1734  exgen  1974  spnfw  1979  r19.29vva  3201  ab0w  4310  rmosn  4658  opthpr  4785  opthprneg  4798  wereu2  5588  relop  5763  frpomin  6247  fpropnf1  7160  soxp  7990  omopth2  8435  swoord2  8550  mapdom2  8960  en3lplem2  9399  rankxplim3  9667  cfsmolem  10054  fin1a2s  10198  fpwwe2lem11  10425  fpwwe2lem12  10426  inawina  10474  gchina  10483  elnnz  12357  xmullem  13026  icossicc  13196  iocssicc  13197  ioossico  13198  ioopnfsup  13612  icopnfsup  13613  expeq0  13841  repswswrd  14525  repswcshw  14553  coprmprod  16394  vdwlem6  16715  lublecllem  18106  tsrlemax  18332  ablsimpnosubgd  19735  ocv2ss  20906  issubassa3  21100  0top  22161  neindisj2  22302  lmconst  22440  cnpresti  22467  sslm  22478  cmpfi  22587  dfconn2  22598  hausflim  23160  bndth  24149  nmoleub2a  24308  nmoleub2b  24309  cmetcaulem  24480  ioorf  24765  ioorinv2  24767  dgrcolem2  25463  plydiveu  25486  dvloglem  25831  lmieu  27173  axcontlem4  27363  clwwlknwwlksn  28430  numclwwlk1lem2foa  28746  dipsubdir  29238  omssubadd  32295  subgrpth  33124  idinside  34414  endofsegid  34415  nn0prpwlem  34539  meran1  34628  onsuct0  34658  bj-sngltag  35201  poimirlem26  35831  ftc1anclem7  35884  fdc1  35932  rngosubdi  36131  rngosubdir  36132  mpobi123f  36348  lkreqN  37210  cdlemg33a  38746  mapdordlem2  39677  cnvtrucl0  41256  ntrneiiso  41725  3ornot23  42153  rspsbc2  42178  sbcim2g  42182  idn2  42257  idn3  42259  trsspwALT2  42463  sspwtrALT  42466  sstrALT2  42479  r19.36vf  42709  ioossioc  43065  ioossioobi  43090  stoweidlem27  43603  stoweidlem31  43607  stoweidlem60  43636  hoidmvlelem3  44171  atbiffatnnb  44447  cfsetsnfsetf1  44593  el1fzopredsuc  44857  poprelb  45016  upwlkwlk  45341  line2y  46141  elsetrecslem  46444