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  168  pm2.6  193  pm2.65  195  ancld  553  ancrd  554  anim12d  610  anim1d  612  anim2d  613  orel2  887  pm2.621  895  pm2.63  937  orim1d  962  orim2d  963  ecase2d  1026  cad0  1618  merco2  1737  exgen  1978  spnfw  1984  rmosn  4657  opthpr  4784  opthprneg  4797  wereu2  5554  relop  5723  fpropnf1  7027  soxp  7825  omopth2  8212  swoord2  8323  mapdom2  8690  en3lplem2  9078  rankxplim3  9312  cfsmolem  9694  fin1a2s  9838  fpwwe2lem12  10065  fpwwe2lem13  10066  inawina  10114  gchina  10123  elnnz  11994  xmullem  12660  icossicc  12827  iocssicc  12828  ioossico  12829  ioopnfsup  13235  icopnfsup  13236  expeq0  13462  repswswrd  14148  repswcshw  14176  coprmprod  16007  vdwlem6  16324  lublecllem  17600  tsrlemax  17832  ablsimpnosubgd  19228  issubassa3  20099  ocv2ss  20819  0top  21593  neindisj2  21733  lmconst  21871  cnpresti  21898  sslm  21909  cmpfi  22018  dfconn2  22029  hausflim  22591  bndth  23564  nmoleub2a  23723  nmoleub2b  23724  cmetcaulem  23893  ioorf  24176  ioorinv2  24178  dgrcolem2  24866  plydiveu  24889  dvloglem  25233  lmieu  26572  axcontlem4  26755  clwwlknwwlksn  27818  numclwwlk1lem2foa  28135  dipsubdir  28627  omssubadd  31560  subgrpth  32383  frpomin  33080  idinside  33547  endofsegid  33548  nn0prpwlem  33672  meran1  33761  onsuct0  33791  bj-sngltag  34297  poimirlem26  34920  ftc1anclem7  34975  fdc1  35023  rngosubdi  35225  rngosubdir  35226  mpobi123f  35442  lkreqN  36308  cdlemg33a  37844  mapdordlem2  38775  cnvtrucl0  39991  ntrneiiso  40448  3ornot23  40850  rspsbc2  40875  sbcim2g  40879  idn2  40954  idn3  40956  trsspwALT2  41160  sspwtrALT  41163  sstrALT2  41176  r19.36vf  41411  ioossioc  41773  ioossioobi  41800  stoweidlem27  42319  stoweidlem31  42323  stoweidlem60  42352  hoidmvlelem3  42886  atbiffatnnb  43155  el1fzopredsuc  43532  poprelb  43693  upwlkwlk  44021  line2y  44749  elsetrecslem  44808