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  192  pm2.65  194  ancld  555  ancrd  556  anim12d  615  anim1d  617  anim2d  618  orel2  896  pm2.621  904  pm2.63  948  orim1d  973  orim2d  974  cad0  1625  merco2  1743  exgen  1981  spnfw  1986  r19.29vva  3200  rmosn  4658  opthpr  4789  opthprneg  4803  wereu2  5622  relop  5799  frpomin  6298  fpropnf1  7218  soxp  8076  omopth2  8516  swoord2  8674  mapdom2  9083  en3lplem2  9532  rankxplim3  9803  cfsmolem  10190  fin1a2s  10334  fpwwe2lem11  10562  fpwwe2lem12  10563  inawina  10611  gchina  10620  elnnz  12532  xmullem  13214  icossicc  13387  iocssicc  13388  ioossico  13389  ioopnfsup  13821  icopnfsup  13822  expeq0  14052  repswswrd  14744  repswcshw  14772  coprmprod  16628  vdwlem6  16955  lublecllem  18322  tsrlemax  18550  chnccat  18590  ablsimpnosubgd  20079  ocv2ss  21655  issubassa3  21848  0top  22973  neindisj2  23113  lmconst  23251  cnpresti  23278  sslm  23289  cmpfi  23398  dfconn2  23409  hausflim  23971  bndth  24950  nmoleub2a  25109  nmoleub2b  25110  cmetcaulem  25280  ioorf  25565  ioorinv2  25567  dvfsumlem2  26019  dgrcolem2  26264  plydiveu  26289  taylthlem2  26364  dvloglem  26637  elnnzs  28418  expsne0  28453  bdayfinbndlem1  28484  lmieu  28877  axcontlem4  29061  clwwlknwwlksn  30133  numclwwlk1lem2foa  30449  dipsubdir  30944  omssubadd  34491  subgrpth  35369  idinside  36319  endofsegid  36320  nn0prpwlem  36557  meran1  36646  onsuct0  36676  weiunso  36701  bj-axdd2ALT  36967  bj-sngltag  37343  poimirlem26  38020  ftc1anclem7  38073  fdc1  38120  rngosubdi  38319  rngosubdir  38320  mpobi123f  38536  lkreqN  39669  cdlemg33a  41205  mapdordlem2  42136  fimgmcyc  43027  onsucf1olem  43722  cnvtrucl0  44075  ntrneiiso  44542  3ornot23  44960  rspsbc2  44985  sbcim2g  44989  idn2  45064  idn3  45066  trsspwALT2  45269  sspwtrALT  45272  sstrALT2  45285  r19.36vf  45590  ioossioc  45944  ioossioobi  45969  stoweidlem27  46477  stoweidlem31  46481  stoweidlem60  46510  hoidmvlelem3  47047  chnerlem3  47336  atbiffatnnb  47382  cfsetsnfsetf1  47529  el1fzopredsuc  47796  poprelb  48006  isubgr3stgrlem4  48467  upwlkwlk  48637  line2y  49253  elsetrecslem  50196