Theorem idd 25

Description: Principle of identity id 23 with antecedent. (Contributed by NM, 26-Nov-1995.)

Assertion

Ref	Expression
idd	⊢ (𝜑 → (𝜓 → 𝜓))

Proof of Theorem idd

Step	Hyp	Ref	Expression
1		id 23	. 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  83  simprim  167  pm2.6  193  pm2.65  195  ancld  559  ancrd  560  anim12d  620  anim1d  622  anim2d  623  orel2  903  pm2.621  911  pm2.63  955  orim1d  981  orim2d  982  cad0  1641  merco2  1759  exgen  1997  spnfw  2002  r19.29vva  3225  rmosn  4681  opthpr  4812  opthprneg  4826  wereu2  5649  relop  5827  frpomin  6331  fpropnf1  7255  soxp  8113  omopth2  8557  swoord2  8716  mapdom2  9124  en3lplem2  9570  rankxplim3  9841  cfsmolem  10242  fin1a2s  10386  fpwwe2lem11  10614  fpwwe2lem12  10615  inawina  10663  gchina  10672  elnnz  12592  xmullem  13281  icossicc  13454  iocssicc  13455  ioossico  13456  ioopnfsup  13888  icopnfsup  13889  expeq0  14119  repswswrd  14811  repswcshw  14839  coprmprod  16709  vdwlem6  17036  lublecllem  18404  tsrlemax  18632  chnccat  18672  ablsimpnosubgd  20167  ocv2ss  21783  issubassa3  21976  0top  23101  neindisj2  23241  lmconst  23379  cnpresti  23406  sslm  23417  cmpfi  23526  dfconn2  23537  hausflim  24099  bndth  25078  nmoleub2a  25237  nmoleub2b  25238  cmetcaulem  25408  ioorf  25693  ioorinv2  25695  dvfsumlem2  26147  dgrcolem2  26392  plydiveu  26420  taylthlem2  26495  dvloglem  26771  elnnzs  28552  expsne0  28587  bdayfinbndlem1  28618  lmieu  29036  axcontlem4  29226  clwwlknwwlksn  30298  numclwwlk1lem2foa  30614  dipsubdir  31109  omssubadd  34607  subgrpth  35497  idinside  36447  endofsegid  36448  nn0prpwlem  36695  meran1  36784  onsuct0  36814  weiunso  36839  bj-axdd2ALT  37104  bj-sngltag  37480  poimirlem26  38157  ftc1anclem7  38210  fdc1  38257  rngosubdi  38456  rngosubdir  38457  mpobi123f  38673  lkreqN  39806  cdlemg33a  41342  mapdordlem2  42273  fimgmcyc  43164  onsucf1olem  43859  cnvtrucl0  44212  ntrneiiso  44679  3ornot23  45083  rspsbc2  45108  sbcim2g  45112  idn2  45187  idn3  45189  trsspwALT2  45392  sspwtrALT  45395  sstrALT2  45408  r19.36vf  45712  ioossioc  46066  ioossioobi  46091  stoweidlem27  46599  stoweidlem31  46603  stoweidlem60  46632  hoidmvlelem3  47169  chnerlem3  47458  atbiffatnnb  47504  cfsetsnfsetf1  47651  el1fzopredsuc  47918  poprelb  48128  isubgr3stgrlem4  48589  upwlkwlk  48759  line2y  49386  elsetrecslem  50328