Theorem idd 24

Description: Principle of identity id 22 with antecedent. (Contributed by NM, 26-Nov-1995.)

Assertion

Ref	Expression
idd	|- ( ph -> ( ps -> ps ) )

Proof of Theorem idd

Step	Hyp	Ref	Expression
1		id 22	. 2 |- ( ps -> ps )
2	1	a1i 11	1 |- ( ph -> ( ps -> ps ) )

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  162  pm2.6  182  pm2.65  184  orel2  398  pm2.621  424  simpr  477  ancld  576  ancrd  577  anim12d  586  anim1d  588  anim2d  589  pm2.63  829  orim1d  884  orim2d  885  ecase2d  981  cad0  1556  merco2  1661  spnfw  1928  eqsbc3rOLD  3493  opthpr  4384  wereu2  5111  relop  5272  fpropnf1  6524  soxp  7290  omopth2  7664  swoord2  7774  mapdom2  8131  en3lplem2  8512  rankxplim3  8744  cfsmolem  9092  fin1a2s  9236  fpwwe2lem12  9463  fpwwe2lem13  9464  inawina  9512  gchina  9521  elnnz  11387  xmullem  12094  icossicc  12260  iocssicc  12261  ioossico  12262  ioopnfsup  12663  icopnfsup  12664  expeq0  12890  repswswrd  13531  repswcshw  13558  coprmprod  15375  vdwlem6  15690  lublecllem  16988  tsrlemax  17220  ocv2ss  20017  0top  20787  neindisj2  20927  lmconst  21065  cnpresti  21092  sslm  21103  cmpfi  21211  dfconn2  21222  hausflim  21785  bndth  22757  nmoleub2a  22917  nmoleub2b  22918  cmetcaulem  23086  ioorf  23341  ioorinv2  23343  dgrcolem2  24030  plydiveu  24053  dvloglem  24394  lmieu  25676  axcontlem4  25847  clwwlksnwwlksn  27209  numclwlk1lem2foa  27224  dipsubdir  27703  omssubadd  30362  idinside  32191  endofsegid  32192  nn0prpwlem  32317  nn0prpw  32318  meran1  32410  onsuct0  32440  bj-sngltag  32971  poimirlem26  33435  ftc1anclem7  33491  fdc1  33542  rngosubdi  33744  rngosubdir  33745  mpt2bi123f  33971  lkreqN  34457  cdlemg33a  35994  mapdordlem2  36926  cnvtrucl0  37931  ntrneiiso  38389  3ornot23  38715  rspsbc2  38744  sbcim2g  38748  idn2  38838  idn3  38840  trsspwALT2  39046  sspwtrALT  39049  sstrALT2  39070  r19.36vf  39324  ioossioc  39713  ioossioobi  39743  stoweidlem27  40244  stoweidlem31  40248  stoweidlem60  40277  hoidmvlelem3  40811  atbiffatnnb  41079  el1fzopredsuc  41335  upwlkwlk  41720  elsetrecslem  42444