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  890  pm2.621  898  pm2.63  942  orim1d  967  orim2d  968  cad0  1614  merco2  1732  exgen  1971  spnfw  1976  r19.29vva  3213  ab0w  4384  rmosn  4723  opthpr  4855  opthprneg  4869  wereu2  5685  relop  5863  frpomin  6362  fpropnf1  7286  soxp  8152  omopth2  8620  swoord2  8776  mapdom2  9186  en3lplem2  9650  rankxplim3  9918  cfsmolem  10307  fin1a2s  10451  fpwwe2lem11  10678  fpwwe2lem12  10679  inawina  10727  gchina  10736  elnnz  12620  xmullem  13302  icossicc  13472  iocssicc  13473  ioossico  13474  ioopnfsup  13900  icopnfsup  13901  expeq0  14129  repswswrd  14818  repswcshw  14846  coprmprod  16694  vdwlem6  17019  lublecllem  18417  tsrlemax  18643  ablsimpnosubgd  20138  ocv2ss  21708  issubassa3  21903  0top  23005  neindisj2  23146  lmconst  23284  cnpresti  23311  sslm  23322  cmpfi  23431  dfconn2  23442  hausflim  24004  bndth  25003  nmoleub2a  25163  nmoleub2b  25164  cmetcaulem  25335  ioorf  25621  ioorinv2  25623  dvfsumlem2  26081  dgrcolem2  26328  plydiveu  26354  taylthlem2  26430  dvloglem  26704  elnnzs  28401  expsne0  28428  lmieu  28806  axcontlem4  28996  clwwlknwwlksn  30066  numclwwlk1lem2foa  30382  dipsubdir  30876  omssubadd  34281  subgrpth  35118  idinside  36065  endofsegid  36066  nn0prpwlem  36304  meran1  36393  onsuct0  36423  weiunso  36448  bj-sngltag  36965  poimirlem26  37632  ftc1anclem7  37685  fdc1  37732  rngosubdi  37931  rngosubdir  37932  mpobi123f  38148  lkreqN  39151  cdlemg33a  40688  mapdordlem2  41619  fimgmcyc  42520  onsucf1olem  43259  cnvtrucl0  43613  ntrneiiso  44080  3ornot23  44506  rspsbc2  44531  sbcim2g  44535  idn2  44610  idn3  44612  trsspwALT2  44816  sspwtrALT  44819  sstrALT2  44832  r19.36vf  45075  ioossioc  45444  ioossioobi  45469  stoweidlem27  45982  stoweidlem31  45986  stoweidlem60  46015  hoidmvlelem3  46552  atbiffatnnb  46861  cfsetsnfsetf1  47008  el1fzopredsuc  47274  poprelb  47448  isubgr3stgrlem4  47871  upwlkwlk  47982  line2y  48604  elsetrecslem  48929