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  1648  merco2  1766  exgen  2004  spnfw  2009  r19.29vva  3225  rmosn  4686  opthpr  4817  opthprneg  4831  wereu2  5660  relop  5838  frpomin  6343  fpropnf1  7267  soxp  8126  omopth2  8570  swoord2  8729  mapdom2  9137  en3lplem2  9583  rankxplim3  9854  cfsmolem  10255  fin1a2s  10399  fpwwe2lem11  10627  fpwwe2lem12  10628  inawina  10676  gchina  10685  elnnz  12602  xmullem  13291  icossicc  13464  iocssicc  13465  ioossico  13466  ioopnfsup  13899  icopnfsup  13900  expeq0  14130  repswswrd  14823  repswcshw  14851  coprmprod  16720  vdwlem6  17047  lublecllem  18415  tsrlemax  18643  chnccat  18683  ablsimpnosubgd  20177  ocv2ss  21804  issubassa3  21997  0top  23121  neindisj2  23261  lmconst  23399  cnpresti  23426  sslm  23437  cmpfi  23546  dfconn2  23557  hausflim  24119  bndth  25098  nmoleub2a  25257  nmoleub2b  25258  cmetcaulem  25428  ioorf  25713  ioorinv2  25715  dvfsumlem2  26167  dgrcolem2  26412  plydiveu  26440  taylthlem2  26515  dvloglem  26791  elnnzs  28572  expsne0  28607  bdayfinbndlem1  28638  lmieu  29071  axcontlem4  29295  clwwlknwwlksn  30367  numclwwlk1lem2foa  30683  dipsubdir  31178  omssubadd  34668  subgrpth  35604  idinside  36554  endofsegid  36555  nn0prpwlem  36811  meran1  36900  onsuct0  36930  weiunso  36955  bj-axdd2ALT  37220  bj-sngltag  37597  poimirlem26  38275  ftc1anclem7  38328  fdc1  38375  rngosubdi  38574  rngosubdir  38575  mpobi123f  38789  lkreqN  39922  cdlemg33a  41458  mapdordlem2  42389  fimgmcyc  43282  onsucf1olem  43977  cnvtrucl0  44330  ntrneiiso  44797  3ornot23  45198  rspsbc2  45223  sbcim2g  45227  idn2  45302  idn3  45304  trsspwALT2  45507  sspwtrALT  45510  sstrALT2  45523  r19.36vf  45834  ioossioc  46188  ioossioobi  46213  stoweidlem27  46721  stoweidlem31  46725  stoweidlem60  46754  hoidmvlelem3  47291  chnerlem3  47580  atbiffatnnb  47626  cfsetsnfsetf1  47773  el1fzopredsuc  48040  poprelb  48250  isubgr3stgrlem4  48711  upwlkwlk  48881  line2y  49512  elsetrecslem  50454