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  163  pm2.6  182  pm2.65  184  simprOLD  472  ancld  534  ancrd  535  anim12d  590  anim1d  592  anim2d  593  orel2  869  pm2.621  876  pm2.63  917  orim1d  940  orim2d  941  ecase2d  1016  cad0  1704  merco2  1809  spnfw  2086  opthpr  4516  opthprneg  4532  wereu2  5247  relop  5412  fpropnf1  6668  soxp  7442  omopth2  7819  swoord2  7929  mapdom2  8288  en3lplem2  8673  rankxplim3  8909  cfsmolem  9295  fin1a2s  9439  fpwwe2lem12  9666  fpwwe2lem13  9667  inawina  9715  gchina  9724  elnnz  11590  xmullem  12300  icossicc  12467  iocssicc  12468  ioossico  12469  ioopnfsup  12872  icopnfsup  12873  expeq0  13098  repswswrd  13741  repswcshw  13768  coprmprod  15583  vdwlem6  15898  lublecllem  17197  tsrlemax  17429  ocv2ss  20235  0top  21009  neindisj2  21149  lmconst  21287  cnpresti  21314  sslm  21325  cmpfi  21433  dfconn2  21444  hausflim  22006  bndth  22978  nmoleub2a  23137  nmoleub2b  23138  cmetcaulem  23306  ioorf  23562  ioorinv2  23564  dgrcolem2  24251  plydiveu  24274  dvloglem  24616  lmieu  25898  axcontlem4  26069  clwwlknwwlksn  27194  clwwlknwwlksnOLD  27195  clwwlknonwwlknonb  27282  numclwwlk1lem2foa  27541  dipsubdir  28044  omssubadd  30703  frpomin  32076  idinside  32529  endofsegid  32530  nn0prpwlem  32655  nn0prpw  32656  meran1  32748  onsuct0  32778  bj-sngltag  33303  poimirlem26  33769  ftc1anclem7  33824  fdc1  33875  rngosubdi  34077  rngosubdir  34078  mpt2bi123f  34304  lkreqN  34980  cdlemg33a  36516  mapdordlem2  37448  cnvtrucl0  38458  ntrneiiso  38916  3ornot23  39241  rspsbc2  39270  sbcim2g  39274  idn2  39364  idn3  39366  trsspwALT2  39572  sspwtrALT  39575  sstrALT2  39593  r19.36vf  39846  ioossioc  40235  ioossioobi  40263  stoweidlem27  40762  stoweidlem31  40766  stoweidlem60  40795  hoidmvlelem3  41332  atbiffatnnb  41600  el1fzopredsuc  41864  upwlkwlk  42249  elsetrecslem  42974