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  190  pm2.65  192  ancld  549  ancrd  550  anim12d  607  anim1d  609  anim2d  610  orel2  888  pm2.621  896  pm2.63  938  orim1d  963  orim2d  964  ecase2dOLD  1028  cad0  1611  cad0OLD  1612  merco2  1730  exgen  1970  spnfw  1975  r19.29vva  3203  ab0w  4375  rmosn  4725  opthpr  4854  opthprneg  4867  wereu2  5675  relop  5853  frpomin  6348  fpropnf1  7277  soxp  8134  omopth2  8605  swoord2  8757  mapdom2  9176  en3lplem2  9643  rankxplim3  9911  cfsmolem  10300  fin1a2s  10444  fpwwe2lem11  10671  fpwwe2lem12  10672  inawina  10720  gchina  10729  elnnz  12606  xmullem  13283  icossicc  13453  iocssicc  13454  ioossico  13455  ioopnfsup  13870  icopnfsup  13871  expeq0  14098  repswswrd  14778  repswcshw  14806  coprmprod  16648  vdwlem6  16974  lublecllem  18371  tsrlemax  18597  ablsimpnosubgd  20090  ocv2ss  21639  issubassa3  21833  0top  22947  neindisj2  23088  lmconst  23226  cnpresti  23253  sslm  23264  cmpfi  23373  dfconn2  23384  hausflim  23946  bndth  24945  nmoleub2a  25105  nmoleub2b  25106  cmetcaulem  25277  ioorf  25563  ioorinv2  25565  dvfsumlem2  26022  dgrcolem2  26271  plydiveu  26295  taylthlem2  26371  dvloglem  26644  lmieu  28680  axcontlem4  28870  clwwlknwwlksn  29940  numclwwlk1lem2foa  30256  dipsubdir  30750  omssubadd  34071  subgrpth  34895  idinside  35831  endofsegid  35832  nn0prpwlem  35957  meran1  36046  onsuct0  36076  bj-sngltag  36613  poimirlem26  37270  ftc1anclem7  37323  fdc1  37370  rngosubdi  37569  rngosubdir  37570  mpobi123f  37786  lkreqN  38792  cdlemg33a  40329  mapdordlem2  41260  onsucf1olem  42846  cnvtrucl0  43201  ntrneiiso  43668  3ornot23  44095  rspsbc2  44120  sbcim2g  44124  idn2  44199  idn3  44201  trsspwALT2  44405  sspwtrALT  44408  sstrALT2  44421  r19.36vf  44647  ioossioc  45020  ioossioobi  45045  stoweidlem27  45558  stoweidlem31  45562  stoweidlem60  45591  hoidmvlelem3  46128  atbiffatnnb  46437  cfsetsnfsetf1  46584  el1fzopredsuc  46848  poprelb  47006  upwlkwlk  47392  line2y  48019  elsetrecslem  48321