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  610  anim1d  612  anim2d  613  orel2  891  pm2.621  899  pm2.63  943  orim1d  968  orim2d  969  cad0  1620  merco2  1738  exgen  1976  spnfw  1981  r19.29vva  3198  rmosn  4664  opthpr  4795  opthprneg  4809  wereu2  5621  relop  5799  frpomin  6298  fpropnf1  7215  soxp  8072  omopth2  8512  swoord2  8670  mapdom2  9079  en3lplem2  9525  rankxplim3  9796  cfsmolem  10183  fin1a2s  10327  fpwwe2lem11  10555  fpwwe2lem12  10556  inawina  10604  gchina  10613  elnnz  12525  xmullem  13207  icossicc  13380  iocssicc  13381  ioossico  13382  ioopnfsup  13814  icopnfsup  13815  expeq0  14045  repswswrd  14737  repswcshw  14765  coprmprod  16621  vdwlem6  16948  lublecllem  18315  tsrlemax  18543  chnccat  18583  ablsimpnosubgd  20072  ocv2ss  21663  issubassa3  21856  0top  22958  neindisj2  23098  lmconst  23236  cnpresti  23263  sslm  23274  cmpfi  23383  dfconn2  23394  hausflim  23956  bndth  24935  nmoleub2a  25094  nmoleub2b  25095  cmetcaulem  25265  ioorf  25550  ioorinv2  25552  dvfsumlem2  26004  dgrcolem2  26249  plydiveu  26275  taylthlem2  26351  dvloglem  26625  elnnzs  28407  expsne0  28442  bdayfinbndlem1  28473  lmieu  28866  axcontlem4  29050  clwwlknwwlksn  30123  numclwwlk1lem2foa  30439  dipsubdir  30934  omssubadd  34460  subgrpth  35332  idinside  36282  endofsegid  36283  nn0prpwlem  36520  meran1  36609  onsuct0  36639  weiunso  36664  bj-axdd2ALT  36930  bj-sngltag  37306  poimirlem26  37981  ftc1anclem7  38034  fdc1  38081  rngosubdi  38280  rngosubdir  38281  mpobi123f  38497  lkreqN  39630  cdlemg33a  41166  mapdordlem2  42097  fimgmcyc  42993  onsucf1olem  43716  cnvtrucl0  44069  ntrneiiso  44536  3ornot23  44954  rspsbc2  44979  sbcim2g  44983  idn2  45058  idn3  45060  trsspwALT2  45263  sspwtrALT  45266  sstrALT2  45279  r19.36vf  45584  ioossioc  45940  ioossioobi  45965  stoweidlem27  46473  stoweidlem31  46477  stoweidlem60  46506  hoidmvlelem3  47043  chnerlem3  47330  atbiffatnnb  47372  cfsetsnfsetf1  47519  el1fzopredsuc  47786  poprelb  47996  isubgr3stgrlem4  48457  upwlkwlk  48627  line2y  49243  elsetrecslem  50186