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  3205  ab0w  4359  rmosn  4700  opthpr  4832  opthprneg  4846  wereu2  5656  relop  5835  frpomin  6334  fpropnf1  7265  soxp  8133  omopth2  8601  swoord2  8757  mapdom2  9167  en3lplem2  9632  rankxplim3  9900  cfsmolem  10289  fin1a2s  10433  fpwwe2lem11  10660  fpwwe2lem12  10661  inawina  10709  gchina  10718  elnnz  12603  xmullem  13285  icossicc  13458  iocssicc  13459  ioossico  13460  ioopnfsup  13886  icopnfsup  13887  expeq0  14115  repswswrd  14807  repswcshw  14835  coprmprod  16685  vdwlem6  17011  lublecllem  18375  tsrlemax  18601  ablsimpnosubgd  20092  ocv2ss  21638  issubassa3  21831  0top  22926  neindisj2  23066  lmconst  23204  cnpresti  23231  sslm  23242  cmpfi  23351  dfconn2  23362  hausflim  23924  bndth  24913  nmoleub2a  25073  nmoleub2b  25074  cmetcaulem  25245  ioorf  25531  ioorinv2  25533  dvfsumlem2  25990  dgrcolem2  26237  plydiveu  26263  taylthlem2  26339  dvloglem  26614  elnnzs  28346  expsne0  28378  lmieu  28768  axcontlem4  28951  clwwlknwwlksn  30024  numclwwlk1lem2foa  30340  dipsubdir  30834  omssubadd  34337  subgrpth  35161  idinside  36107  endofsegid  36108  nn0prpwlem  36345  meran1  36434  onsuct0  36464  weiunso  36489  bj-sngltag  37006  poimirlem26  37675  ftc1anclem7  37728  fdc1  37775  rngosubdi  37974  rngosubdir  37975  mpobi123f  38191  lkreqN  39193  cdlemg33a  40730  mapdordlem2  41661  fimgmcyc  42532  onsucf1olem  43269  cnvtrucl0  43623  ntrneiiso  44090  3ornot23  44509  rspsbc2  44534  sbcim2g  44538  idn2  44613  idn3  44615  trsspwALT2  44818  sspwtrALT  44821  sstrALT2  44834  r19.36vf  45140  ioossioc  45501  ioossioobi  45526  stoweidlem27  46036  stoweidlem31  46040  stoweidlem60  46069  hoidmvlelem3  46606  atbiffatnnb  46921  cfsetsnfsetf1  47068  el1fzopredsuc  47334  poprelb  47518  isubgr3stgrlem4  47961  upwlkwlk  48094  line2y  48715  elsetrecslem  49543