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  3193  rmosn  4671  opthpr  4802  opthprneg  4816  wereu2  5616  relop  5794  frpomin  6292  fpropnf1  7207  soxp  8065  omopth2  8505  swoord2  8661  mapdom2  9068  en3lplem2  9510  rankxplim3  9781  cfsmolem  10168  fin1a2s  10312  fpwwe2lem11  10539  fpwwe2lem12  10540  inawina  10588  gchina  10597  elnnz  12485  xmullem  13165  icossicc  13338  iocssicc  13339  ioossico  13340  ioopnfsup  13770  icopnfsup  13771  expeq0  14001  repswswrd  14693  repswcshw  14721  coprmprod  16574  vdwlem6  16900  lublecllem  18266  tsrlemax  18494  chnccat  18534  ablsimpnosubgd  20020  ocv2ss  21612  issubassa3  21805  0top  22899  neindisj2  23039  lmconst  23177  cnpresti  23204  sslm  23215  cmpfi  23324  dfconn2  23335  hausflim  23897  bndth  24885  nmoleub2a  25045  nmoleub2b  25046  cmetcaulem  25216  ioorf  25502  ioorinv2  25504  dvfsumlem2  25961  dgrcolem2  26208  plydiveu  26234  taylthlem2  26310  dvloglem  26585  elnnzs  28326  expsne0  28360  lmieu  28763  axcontlem4  28947  clwwlknwwlksn  30020  numclwwlk1lem2foa  30336  dipsubdir  30830  omssubadd  34334  subgrpth  35199  idinside  36149  endofsegid  36150  nn0prpwlem  36387  meran1  36476  onsuct0  36506  weiunso  36531  bj-sngltag  37048  poimirlem26  37706  ftc1anclem7  37759  fdc1  37806  rngosubdi  38005  rngosubdir  38006  mpobi123f  38222  lkreqN  39289  cdlemg33a  40825  mapdordlem2  41756  fimgmcyc  42652  onsucf1olem  43387  cnvtrucl0  43741  ntrneiiso  44208  3ornot23  44626  rspsbc2  44651  sbcim2g  44655  idn2  44730  idn3  44732  trsspwALT2  44935  sspwtrALT  44938  sstrALT2  44951  r19.36vf  45257  ioossioc  45616  ioossioobi  45641  stoweidlem27  46149  stoweidlem31  46153  stoweidlem60  46182  hoidmvlelem3  46719  chnerlem3  47006  atbiffatnnb  47036  cfsetsnfsetf1  47183  el1fzopredsuc  47449  poprelb  47648  isubgr3stgrlem4  48093  upwlkwlk  48263  line2y  48880  elsetrecslem  49824