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  1618  merco2  1736  exgen  1974  spnfw  1979  r19.29vva  3198  ab0w  4345  rmosn  4686  opthpr  4818  opthprneg  4832  wereu2  5638  relop  5817  frpomin  6316  fpropnf1  7245  soxp  8111  omopth2  8551  swoord2  8707  mapdom2  9118  en3lplem2  9573  rankxplim3  9841  cfsmolem  10230  fin1a2s  10374  fpwwe2lem11  10601  fpwwe2lem12  10602  inawina  10650  gchina  10659  elnnz  12546  xmullem  13231  icossicc  13404  iocssicc  13405  ioossico  13406  ioopnfsup  13833  icopnfsup  13834  expeq0  14064  repswswrd  14756  repswcshw  14784  coprmprod  16638  vdwlem6  16964  lublecllem  18326  tsrlemax  18552  ablsimpnosubgd  20043  ocv2ss  21589  issubassa3  21782  0top  22877  neindisj2  23017  lmconst  23155  cnpresti  23182  sslm  23193  cmpfi  23302  dfconn2  23313  hausflim  23875  bndth  24864  nmoleub2a  25024  nmoleub2b  25025  cmetcaulem  25195  ioorf  25481  ioorinv2  25483  dvfsumlem2  25940  dgrcolem2  26187  plydiveu  26213  taylthlem2  26289  dvloglem  26564  elnnzs  28296  expsne0  28328  lmieu  28718  axcontlem4  28901  clwwlknwwlksn  29974  numclwwlk1lem2foa  30290  dipsubdir  30784  omssubadd  34298  subgrpth  35128  idinside  36079  endofsegid  36080  nn0prpwlem  36317  meran1  36406  onsuct0  36436  weiunso  36461  bj-sngltag  36978  poimirlem26  37647  ftc1anclem7  37700  fdc1  37747  rngosubdi  37946  rngosubdir  37947  mpobi123f  38163  lkreqN  39170  cdlemg33a  40707  mapdordlem2  41638  fimgmcyc  42529  onsucf1olem  43266  cnvtrucl0  43620  ntrneiiso  44087  3ornot23  44506  rspsbc2  44531  sbcim2g  44535  idn2  44610  idn3  44612  trsspwALT2  44815  sspwtrALT  44818  sstrALT2  44831  r19.36vf  45137  ioossioc  45497  ioossioobi  45522  stoweidlem27  46032  stoweidlem31  46036  stoweidlem60  46065  hoidmvlelem3  46602  atbiffatnnb  46917  cfsetsnfsetf1  47064  el1fzopredsuc  47330  poprelb  47529  isubgr3stgrlem4  47972  upwlkwlk  48131  line2y  48748  elsetrecslem  49692