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  610  anim1d  612  anim2d  613  orel2  891  pm2.621  899  pm2.63  943  orim1d  968  orim2d  969  cad0  1620  merco2  1738  exgen  1976  spnfw  1981  r19.29vva  3198  rmosn  4678  opthpr  4809  opthprneg  4823  wereu2  5629  relop  5807  frpomin  6306  fpropnf1  7223  soxp  8081  omopth2  8521  swoord2  8679  mapdom2  9088  en3lplem2  9534  rankxplim3  9805  cfsmolem  10192  fin1a2s  10336  fpwwe2lem11  10564  fpwwe2lem12  10565  inawina  10613  gchina  10622  elnnz  12510  xmullem  13191  icossicc  13364  iocssicc  13365  ioossico  13366  ioopnfsup  13796  icopnfsup  13797  expeq0  14027  repswswrd  14719  repswcshw  14747  coprmprod  16600  vdwlem6  16926  lublecllem  18293  tsrlemax  18521  chnccat  18561  ablsimpnosubgd  20047  ocv2ss  21640  issubassa3  21833  0top  22939  neindisj2  23079  lmconst  23217  cnpresti  23244  sslm  23255  cmpfi  23364  dfconn2  23375  hausflim  23937  bndth  24925  nmoleub2a  25085  nmoleub2b  25086  cmetcaulem  25256  ioorf  25542  ioorinv2  25544  dvfsumlem2  26001  dgrcolem2  26248  plydiveu  26274  taylthlem2  26350  dvloglem  26625  elnnzs  28409  expsne0  28444  bdayfinbndlem1  28475  lmieu  28868  axcontlem4  29052  clwwlknwwlksn  30125  numclwwlk1lem2foa  30441  dipsubdir  30935  omssubadd  34477  subgrpth  35347  idinside  36297  endofsegid  36298  nn0prpwlem  36535  meran1  36624  onsuct0  36654  weiunso  36679  bj-axdd2ALT  36865  bj-sngltag  37225  poimirlem26  37891  ftc1anclem7  37944  fdc1  37991  rngosubdi  38190  rngosubdir  38191  mpobi123f  38407  lkreqN  39540  cdlemg33a  41076  mapdordlem2  42007  fimgmcyc  42898  onsucf1olem  43621  cnvtrucl0  43974  ntrneiiso  44441  3ornot23  44859  rspsbc2  44884  sbcim2g  44888  idn2  44963  idn3  44965  trsspwALT2  45168  sspwtrALT  45171  sstrALT2  45184  r19.36vf  45489  ioossioc  45846  ioossioobi  45871  stoweidlem27  46379  stoweidlem31  46383  stoweidlem60  46412  hoidmvlelem3  46949  chnerlem3  47236  atbiffatnnb  47266  cfsetsnfsetf1  47413  el1fzopredsuc  47679  poprelb  47878  isubgr3stgrlem4  48323  upwlkwlk  48493  line2y  49109  elsetrecslem  50052