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  1619  merco2  1737  exgen  1975  spnfw  1980  r19.29vva  3192  ab0w  4329  rmosn  4672  opthpr  4803  opthprneg  4817  wereu2  5613  relop  5790  frpomin  6287  fpropnf1  7201  soxp  8059  omopth2  8499  swoord2  8655  mapdom2  9061  en3lplem2  9503  rankxplim3  9771  cfsmolem  10158  fin1a2s  10302  fpwwe2lem11  10529  fpwwe2lem12  10530  inawina  10578  gchina  10587  elnnz  12475  xmullem  13160  icossicc  13333  iocssicc  13334  ioossico  13335  ioopnfsup  13765  icopnfsup  13766  expeq0  13996  repswswrd  14688  repswcshw  14716  coprmprod  16569  vdwlem6  16895  lublecllem  18261  tsrlemax  18489  chnccat  18529  ablsimpnosubgd  20016  ocv2ss  21608  issubassa3  21801  0top  22896  neindisj2  23036  lmconst  23174  cnpresti  23201  sslm  23212  cmpfi  23321  dfconn2  23332  hausflim  23894  bndth  24882  nmoleub2a  25042  nmoleub2b  25043  cmetcaulem  25213  ioorf  25499  ioorinv2  25501  dvfsumlem2  25958  dgrcolem2  26205  plydiveu  26231  taylthlem2  26307  dvloglem  26582  elnnzs  28323  expsne0  28357  lmieu  28760  axcontlem4  28943  clwwlknwwlksn  30013  numclwwlk1lem2foa  30329  dipsubdir  30823  omssubadd  34308  subgrpth  35166  idinside  36117  endofsegid  36118  nn0prpwlem  36355  meran1  36444  onsuct0  36474  weiunso  36499  bj-sngltag  37016  poimirlem26  37685  ftc1anclem7  37738  fdc1  37785  rngosubdi  37984  rngosubdir  37985  mpobi123f  38201  lkreqN  39208  cdlemg33a  40744  mapdordlem2  41675  fimgmcyc  42566  onsucf1olem  43302  cnvtrucl0  43656  ntrneiiso  44123  3ornot23  44541  rspsbc2  44566  sbcim2g  44570  idn2  44645  idn3  44647  trsspwALT2  44850  sspwtrALT  44853  sstrALT2  44866  r19.36vf  45172  ioossioc  45531  ioossioobi  45556  stoweidlem27  46064  stoweidlem31  46068  stoweidlem60  46097  hoidmvlelem3  46634  atbiffatnnb  46942  cfsetsnfsetf1  47089  el1fzopredsuc  47355  poprelb  47554  isubgr3stgrlem4  47999  upwlkwlk  48169  line2y  48786  elsetrecslem  49730