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  169  pm2.6  194  pm2.65  196  ancld  554  ancrd  555  anim12d  611  anim1d  613  anim2d  614  orel2  888  pm2.621  896  pm2.63  938  orim1d  963  orim2d  964  ecase2d  1027  cad0  1619  merco2  1738  exgen  1978  spnfw  1984  rmosn  4615  opthpr  4742  opthprneg  4755  wereu2  5516  relop  5685  fpropnf1  7003  soxp  7806  omopth2  8193  swoord2  8304  mapdom2  8672  en3lplem2  9060  rankxplim3  9294  cfsmolem  9681  fin1a2s  9825  fpwwe2lem12  10052  fpwwe2lem13  10053  inawina  10101  gchina  10110  elnnz  11979  xmullem  12645  icossicc  12814  iocssicc  12815  ioossico  12816  ioopnfsup  13227  icopnfsup  13228  expeq0  13455  repswswrd  14137  repswcshw  14165  coprmprod  15995  vdwlem6  16312  lublecllem  17590  tsrlemax  17822  ablsimpnosubgd  19219  ocv2ss  20362  issubassa3  20554  0top  21588  neindisj2  21728  lmconst  21866  cnpresti  21893  sslm  21904  cmpfi  22013  dfconn2  22024  hausflim  22586  bndth  23563  nmoleub2a  23722  nmoleub2b  23723  cmetcaulem  23892  ioorf  24177  ioorinv2  24179  dgrcolem2  24871  plydiveu  24894  dvloglem  25239  lmieu  26578  axcontlem4  26761  clwwlknwwlksn  27823  numclwwlk1lem2foa  28139  dipsubdir  28631  omssubadd  31668  subgrpth  32494  frpomin  33191  idinside  33658  endofsegid  33659  nn0prpwlem  33783  meran1  33872  onsuct0  33902  bj-sngltag  34419  poimirlem26  35083  ftc1anclem7  35136  fdc1  35184  rngosubdi  35383  rngosubdir  35384  mpobi123f  35600  lkreqN  36466  cdlemg33a  38002  mapdordlem2  38933  cnvtrucl0  40324  ntrneiiso  40794  3ornot23  41215  rspsbc2  41240  sbcim2g  41244  idn2  41319  idn3  41321  trsspwALT2  41525  sspwtrALT  41528  sstrALT2  41541  r19.36vf  41772  ioossioc  42129  ioossioobi  42154  stoweidlem27  42669  stoweidlem31  42673  stoweidlem60  42702  hoidmvlelem3  43236  atbiffatnnb  43505  el1fzopredsuc  43882  poprelb  44041  upwlkwlk  44367  line2y  45169  elsetrecslem  45228