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  163  pm2.6  182  pm2.65  184  simprOLD  474  ancld  542  ancrd  543  anim12d  598  anim1d  600  anim2d  601  orel2  906  pm2.621  913  pm2.63  955  orim1d  979  orim2d  980  ecase2d  1045  cad0  1711  merco2  1816  spnfw  2099  opthpr  4567  opthprneg  4583  wereu2  5305  relop  5471  fpropnf1  6745  soxp  7521  omopth2  7898  swoord2  8008  mapdom2  8367  en3lplem2  8752  rankxplim3  8988  cfsmolem  9374  fin1a2s  9518  fpwwe2lem12  9745  fpwwe2lem13  9746  inawina  9794  gchina  9803  elnnz  11649  xmullem  12308  icossicc  12475  iocssicc  12476  ioossico  12477  ioopnfsup  12883  icopnfsup  12884  expeq0  13109  repswswrd  13751  repswcshw  13778  coprmprod  15589  vdwlem6  15903  lublecllem  17189  tsrlemax  17421  ocv2ss  20223  0top  20997  neindisj2  21137  lmconst  21275  cnpresti  21302  sslm  21313  cmpfi  21421  dfconn2  21432  hausflim  21994  bndth  22966  nmoleub2a  23125  nmoleub2b  23126  cmetcaulem  23294  ioorf  23550  ioorinv2  23552  dgrcolem2  24240  plydiveu  24263  dvloglem  24604  lmieu  25886  axcontlem4  26057  clwwlknwwlksn  27182  clwwlknwwlksnOLD  27183  clwwlknonwwlknonb  27270  numclwwlk1lem2foa  27529  dipsubdir  28028  omssubadd  30684  frpomin  32056  idinside  32509  endofsegid  32510  nn0prpwlem  32635  nn0prpw  32636  meran1  32724  onsuct0  32754  bj-sngltag  33278  poimirlem26  33745  ftc1anclem7  33800  fdc1  33850  rngosubdi  34052  rngosubdir  34053  mpt2bi123f  34278  lkreqN  34947  cdlemg33a  36484  mapdordlem2  37415  cnvtrucl0  38428  ntrneiiso  38886  3ornot23  39210  rspsbc2  39239  sbcim2g  39243  idn2  39333  idn3  39335  trsspwALT2  39540  sspwtrALT  39543  sstrALT2  39561  r19.36vf  39812  ioossioc  40194  ioossioobi  40221  stoweidlem27  40720  stoweidlem31  40724  stoweidlem60  40753  hoidmvlelem3  41290  atbiffatnnb  41558  el1fzopredsuc  41907  upwlkwlk  42285  elsetrecslem  43010