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  1619  merco2  1737  exgen  1975  spnfw  1980  r19.29vva  3196  rmosn  4676  opthpr  4807  opthprneg  4821  wereu2  5621  relop  5799  frpomin  6298  fpropnf1  7213  soxp  8071  omopth2  8511  swoord2  8668  mapdom2  9076  en3lplem2  9522  rankxplim3  9793  cfsmolem  10180  fin1a2s  10324  fpwwe2lem11  10552  fpwwe2lem12  10553  inawina  10601  gchina  10610  elnnz  12498  xmullem  13179  icossicc  13352  iocssicc  13353  ioossico  13354  ioopnfsup  13784  icopnfsup  13785  expeq0  14015  repswswrd  14707  repswcshw  14735  coprmprod  16588  vdwlem6  16914  lublecllem  18281  tsrlemax  18509  chnccat  18549  ablsimpnosubgd  20035  ocv2ss  21628  issubassa3  21821  0top  22927  neindisj2  23067  lmconst  23205  cnpresti  23232  sslm  23243  cmpfi  23352  dfconn2  23363  hausflim  23925  bndth  24913  nmoleub2a  25073  nmoleub2b  25074  cmetcaulem  25244  ioorf  25530  ioorinv2  25532  dvfsumlem2  25989  dgrcolem2  26236  plydiveu  26262  taylthlem2  26338  dvloglem  26613  elnnzs  28397  expsne0  28432  bdayfinbndlem1  28463  lmieu  28856  axcontlem4  29040  clwwlknwwlksn  30113  numclwwlk1lem2foa  30429  dipsubdir  30923  omssubadd  34457  subgrpth  35328  idinside  36278  endofsegid  36279  nn0prpwlem  36516  meran1  36605  onsuct0  36635  weiunso  36660  bj-sngltag  37184  poimirlem26  37843  ftc1anclem7  37896  fdc1  37943  rngosubdi  38142  rngosubdir  38143  mpobi123f  38359  lkreqN  39426  cdlemg33a  40962  mapdordlem2  41893  fimgmcyc  42785  onsucf1olem  43508  cnvtrucl0  43861  ntrneiiso  44328  3ornot23  44746  rspsbc2  44771  sbcim2g  44775  idn2  44850  idn3  44852  trsspwALT2  45055  sspwtrALT  45058  sstrALT2  45071  r19.36vf  45376  ioossioc  45734  ioossioobi  45759  stoweidlem27  46267  stoweidlem31  46271  stoweidlem60  46300  hoidmvlelem3  46837  chnerlem3  47124  atbiffatnnb  47154  cfsetsnfsetf1  47301  el1fzopredsuc  47567  poprelb  47766  isubgr3stgrlem4  48211  upwlkwlk  48381  line2y  48997  elsetrecslem  49940