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  164  pm2.6  183  pm2.65  185  ancld  543  ancrd  544  anim12d  600  anim1d  602  anim2d  603  orel2  875  pm2.621  883  pm2.63  925  orim1d  949  orim2d  950  ecase2d  1013  cad0  1581  merco2  1700  spnfw  1957  rmosn  4534  opthpr  4661  opthprneg  4674  wereu2  5408  relop  5575  fpropnf1  6856  soxp  7634  omopth2  8017  swoord2  8127  mapdom2  8490  en3lplem2  8876  rankxplim3  9110  cfsmolem  9496  fin1a2s  9640  fpwwe2lem12  9867  fpwwe2lem13  9868  inawina  9916  gchina  9925  elnnz  11809  xmullem  12479  icossicc  12646  iocssicc  12647  ioossico  12648  ioopnfsup  13053  icopnfsup  13054  expeq0  13280  repswswrd  14009  repswcshw  14042  coprmprod  15867  vdwlem6  16184  lublecllem  17468  tsrlemax  17700  ocv2ss  20534  0top  21310  neindisj2  21450  lmconst  21588  cnpresti  21615  sslm  21626  cmpfi  21735  dfconn2  21746  hausflim  22308  bndth  23280  nmoleub2a  23439  nmoleub2b  23440  cmetcaulem  23609  ioorf  23892  ioorinv2  23894  dgrcolem2  24582  plydiveu  24605  dvloglem  24947  lmieu  26287  axcontlem4  26471  clwwlknwwlksn  27568  clwwlknonwwlknonb  27649  numclwwlk1lem2foa  27910  numclwwlk1lem2foaOLD  27911  dipsubdir  28417  omssubadd  31235  frpomin  32639  idinside  33106  endofsegid  33107  nn0prpwlem  33231  meran1  33319  onsuct0  33349  bj-sngltag  33853  poimirlem26  34399  ftc1anclem7  34454  fdc1  34503  rngosubdi  34705  rngosubdir  34706  mpobi123f  34924  lkreqN  35791  cdlemg33a  37327  mapdordlem2  38258  cnvtrucl0  39388  ntrneiiso  39845  ablsimpnosubgd  40081  3ornot23  40302  rspsbc2  40327  sbcim2g  40331  idn2  40406  idn3  40408  trsspwALT2  40612  sspwtrALT  40615  sstrALT2  40628  r19.36vf  40864  ioossioc  41232  ioossioobi  41259  stoweidlem27  41778  stoweidlem31  41782  stoweidlem60  41811  hoidmvlelem3  42345  atbiffatnnb  42613  el1fzopredsuc  42966  poprelb  43089  upwlkwlk  43417  line2y  44145  elsetrecslem  44203