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  1651  merco2  1769  exgen  2007  spnfw  2012  r19.29vva  3224  rmosn  4683  opthpr  4814  opthprneg  4828  wereu2  5656  relop  5834  frpomin  6342  fpropnf1  7268  soxp  8131  omopth2  8575  swoord2  8734  mapdom2  9150  en3lplem2  9596  rankxplim3  9867  cfsmolem  10276  fin1a2s  10420  fpwwe2lem11  10654  fpwwe2lem12  10655  inawina  10703  gchina  10712  elnnz  12629  xmullem  13320  icossicc  13493  iocssicc  13494  ioossico  13495  ioopnfsup  13929  icopnfsup  13930  expeq0  14160  repswswrd  14859  repswcshw  14887  coprmprod  16757  vdwlem6  17084  lublecllem  18452  tsrlemax  18680  chnccat  18720  ablsimpnosubgd  20239  ocv2ss  21892  issubassa3  22087  0top  23214  neindisj2  23354  lmconst  23492  cnpresti  23519  sslm  23530  cmpfi  23639  dfconn2  23650  hausflim  24213  bndth  25192  nmoleub2a  25351  nmoleub2b  25352  cmetcaulem  25522  ioorf  25807  ioorinv2  25809  dvfsumlem2  26261  dgrcolem2  26507  plydiveu  26535  taylthlem2  26617  dvloglem  26893  elnnzs  28674  expsne0  28709  bdayfinbndlem1  28740  lmieu  29176  axcontlem4  29432  subgrpth  30243  clwwlknwwlksn  30516  numclwwlk1lem2foa  30842  dipsubdir  31337  omssubadd  34819  idinside  36672  endofsegid  36673  nn0prpwlem  36949  meran1  37038  onsuct0  37068  weiunso  37093  bj-axdd2ALT  37358  bj-sngltag  37735  poimirlem26  38403  ftc1anclem7  38456  fdc1  38504  rngosubdi  38703  rngosubdir  38704  mpobi123f  38918  lkreqN  40051  cdlemg33a  41587  mapdordlem2  42518  fimgmcyc  43424  onsucf1olem  44119  cnvtrucl0  44472  ntrneiiso  44939  3ornot23  45340  rspsbc2  45365  sbcim2g  45369  idn2  45444  idn3  45446  trsspwALT2  45649  sspwtrALT  45652  sstrALT2  45665  r19.36vf  45976  ioossioc  46330  ioossioobi  46355  stoweidlem27  46863  stoweidlem31  46867  stoweidlem60  46896  hoidmvlelem3  47433  chnerlem3  47720  atbiffatnnb  47808  cfsetsnfsetf1  47955  el1fzopredsuc  48222  poprelb  48432  isubgr3stgrlem4  48893  upwlkwlk  49063  line2y  49693  elsetrecslem  50633