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  3197  rmosn  4663  opthpr  4794  opthprneg  4808  wereu2  5628  relop  5805  frpomin  6304  fpropnf1  7222  soxp  8079  omopth2  8519  swoord2  8677  mapdom2  9086  en3lplem2  9534  rankxplim3  9805  cfsmolem  10192  fin1a2s  10336  fpwwe2lem11  10564  fpwwe2lem12  10565  inawina  10613  gchina  10622  elnnz  12534  xmullem  13216  icossicc  13389  iocssicc  13390  ioossico  13391  ioopnfsup  13823  icopnfsup  13824  expeq0  14054  repswswrd  14746  repswcshw  14774  coprmprod  16630  vdwlem6  16957  lublecllem  18324  tsrlemax  18552  chnccat  18592  ablsimpnosubgd  20081  ocv2ss  21653  issubassa3  21846  0top  22948  neindisj2  23088  lmconst  23226  cnpresti  23253  sslm  23264  cmpfi  23373  dfconn2  23384  hausflim  23946  bndth  24925  nmoleub2a  25084  nmoleub2b  25085  cmetcaulem  25255  ioorf  25540  ioorinv2  25542  dvfsumlem2  25994  dgrcolem2  26239  plydiveu  26264  taylthlem2  26339  dvloglem  26612  elnnzs  28393  expsne0  28428  bdayfinbndlem1  28459  lmieu  28852  axcontlem4  29036  clwwlknwwlksn  30108  numclwwlk1lem2foa  30424  dipsubdir  30919  omssubadd  34444  subgrpth  35316  idinside  36266  endofsegid  36267  nn0prpwlem  36504  meran1  36593  onsuct0  36623  weiunso  36648  bj-axdd2ALT  36914  bj-sngltag  37290  poimirlem26  37967  ftc1anclem7  38020  fdc1  38067  rngosubdi  38266  rngosubdir  38267  mpobi123f  38483  lkreqN  39616  cdlemg33a  41152  mapdordlem2  42083  fimgmcyc  42979  onsucf1olem  43698  cnvtrucl0  44051  ntrneiiso  44518  3ornot23  44936  rspsbc2  44961  sbcim2g  44965  idn2  45040  idn3  45042  trsspwALT2  45245  sspwtrALT  45248  sstrALT2  45261  r19.36vf  45566  ioossioc  45922  ioossioobi  45947  stoweidlem27  46455  stoweidlem31  46459  stoweidlem60  46488  hoidmvlelem3  47025  chnerlem3  47314  atbiffatnnb  47360  cfsetsnfsetf1  47507  el1fzopredsuc  47774  poprelb  47984  isubgr3stgrlem4  48445  upwlkwlk  48615  line2y  49231  elsetrecslem  50174