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  550  ancrd  551  anim12d  608  anim1d  610  anim2d  611  orel2  887  pm2.621  895  pm2.63  937  orim1d  962  orim2d  963  ecase2dOLD  1027  cad0  1621  cad0OLD  1622  merco2  1740  exgen  1979  spnfw  1984  r19.29vva  3263  ab0w  4304  rmosn  4652  opthpr  4779  opthprneg  4792  wereu2  5577  relop  5748  frpomin  6228  fpropnf1  7121  soxp  7941  omopth2  8377  swoord2  8488  mapdom2  8884  en3lplem2  9301  rankxplim3  9570  cfsmolem  9957  fin1a2s  10101  fpwwe2lem11  10328  fpwwe2lem12  10329  inawina  10377  gchina  10386  elnnz  12259  xmullem  12927  icossicc  13097  iocssicc  13098  ioossico  13099  ioopnfsup  13512  icopnfsup  13513  expeq0  13741  repswswrd  14425  repswcshw  14453  coprmprod  16294  vdwlem6  16615  lublecllem  17993  tsrlemax  18219  ablsimpnosubgd  19622  ocv2ss  20790  issubassa3  20982  0top  22041  neindisj2  22182  lmconst  22320  cnpresti  22347  sslm  22358  cmpfi  22467  dfconn2  22478  hausflim  23040  bndth  24027  nmoleub2a  24186  nmoleub2b  24187  cmetcaulem  24357  ioorf  24642  ioorinv2  24644  dgrcolem2  25340  plydiveu  25363  dvloglem  25708  lmieu  27049  axcontlem4  27238  clwwlknwwlksn  28303  numclwwlk1lem2foa  28619  dipsubdir  29111  omssubadd  32167  subgrpth  32996  idinside  34313  endofsegid  34314  nn0prpwlem  34438  meran1  34527  onsuct0  34557  bj-sngltag  35100  poimirlem26  35730  ftc1anclem7  35783  fdc1  35831  rngosubdi  36030  rngosubdir  36031  mpobi123f  36247  lkreqN  37111  cdlemg33a  38647  mapdordlem2  39578  cnvtrucl0  41121  ntrneiiso  41590  3ornot23  42018  rspsbc2  42043  sbcim2g  42047  idn2  42122  idn3  42124  trsspwALT2  42328  sspwtrALT  42331  sstrALT2  42344  r19.36vf  42574  ioossioc  42920  ioossioobi  42945  stoweidlem27  43458  stoweidlem31  43462  stoweidlem60  43491  hoidmvlelem3  44025  atbiffatnnb  44294  cfsetsnfsetf1  44440  el1fzopredsuc  44705  poprelb  44864  upwlkwlk  45189  line2y  45989  elsetrecslem  46290