Theorem idd 25

Description: Principle of identity id 23 with antecedent. (Contributed by NM, 26-Nov-1995.)

Assertion

Ref	Expression
idd	⊢ (𝜑 → (𝜓 → 𝜓))

Proof of Theorem idd

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝜓 → 𝜓)
2	1	a1i 11	1 ⊢ (𝜑 → (𝜓 → 𝜓))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  imim1d  83  simprim  167  pm2.6  193  pm2.65  195  ancld  560  ancrd  561  anim12d  621  anim1d  623  anim2d  624  orel2  904  pm2.621  912  pm2.63  955  orim1d  981  orim2d  982  cad0  1650  merco2  1768  exgen  2006  spnfw  2011  r19.29vva  3222  rmosn  4676  opthpr  4805  opthprneg  4819  wereu2  5647  relop  5827  frpomin  6343  fpropnf1  7271  soxp  8143  omopth2  8595  swoord2  8754  mapdom2  9170  en3lplem2  9617  rankxplim3  9901  cfsmolem  10351  fin1a2s  10495  fpwwe2lem11  10729  fpwwe2lem12  10730  inawina  10778  gchina  10787  elnnz  12706  xmullem  13397  icossicc  13570  iocssicc  13571  ioossico  13572  ioopnfsup  14007  icopnfsup  14008  expeq0  14238  repswswrd  14939  repswcshw  14967  coprmprod  16841  vdwlem6  17169  lublecllem  18537  tsrlemax  18765  chnccat  18805  ablsimpnosubgd  20325  ocv2ss  21984  issubassa3  22179  0top  23306  neindisj2  23446  lmconst  23584  cnpresti  23611  sslm  23622  cmpfi  23731  dfconn2  23742  hausflim  24305  bndth  25284  nmoleub2a  25443  nmoleub2b  25444  cmetcaulem  25614  ioorf  25899  ioorinv2  25901  dvfsumlem2  26352  dgrcolem2  26598  plydiveu  26624  taylthlem2  26706  dvloglem  26981  elnnzs  28792  expsne0  28827  bdayfinbndlem1  28858  lmieu  29294  axcontlem4  29550  subgrpth  30361  clwwlknwwlksn  30634  numclwwlk1lem2foa  30960  dipsubdir  31455  rmo6  35756  onprcf1acwevdlem1  35964  mirimanoffr  36546  idinside  36941  endofsegid  36942  nn0prpwlem  37202  meran1  37291  onsuct0  37321  weiunso  37346  bj-axdd2ALT  37611  bj-sngltag  37988  poimirlem26  38657  ftc1anclem7  38710  fdc1  38773  rngosubdi  38972  rngosubdir  38973  mpobi123f  39187  lkreqN  40320  cdlemg33a  41856  mapdordlem2  42787  fimgmcyc  43691  onsucf1olem  44365  cnvtrucl0  44717  ntrneiiso  45184  3ornot23  45585  rspsbc2  45610  sbcim2g  45614  idn2  45689  idn3  45691  trsspwALT2  45894  sspwtrALT  45897  sstrALT2  45910  r19.36vf  46244  ioossioc  46597  ioossioobi  46622  stoweidlem27  47130  stoweidlem31  47134  stoweidlem60  47163  hoidmvlelem3  47700  chnerlem3  47987  atbiffatnnb  48075  cfsetsnfsetf1  48222  el1fzopredsuc  48489  poprelb  48699  isubgr3stgrlem4  49160  upwlkwlk  49330  line2y  49960  elsetrecslem  50960