MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  idd Structured version   Unicode version

Theorem idd 24
Description: Principle of identity with antecedent. (Contributed by NM, 26-Nov-1995.)
Assertion
Ref Expression
idd  |-  ( ph  ->  ( ps  ->  ps ) )

Proof of Theorem idd
StepHypRef Expression
1 id 22 . 2  |-  ( ps 
->  ps )
21a1i 11 1  |-  ( ph  ->  ( ps  ->  ps ) )
Colors of variables: wff setvar class
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  75  simprim  150  pm2.6  170  pm2.65  172  orel2  381  pm2.621  406  simpr  459  ancld  551  ancrd  552  anim12d  561  anim1d  562  anim2d  563  pm2.63  786  orim1d  837  orim2d  838  ecase2d  938  cad0  1475  merco2  1576  spnfw  1793  r19.36v  2930  r19.44v  2939  r19.45v  2940  eqsbc3r  3309  reuss  3704  opthpr  4122  wereu2  4790  relop  5066  soxp  6812  omopth2  7151  swoord2  7259  mapdom2  7607  en3lplem2  7946  rankxplim3  8212  cfsmolem  8563  fin1a2s  8707  fpwwe2lem12  8930  fpwwe2lem13  8931  inawina  8979  gchina  8988  elnnz  10791  xmullem  11377  icossicc  11532  iocssicc  11533  ioossico  11534  ioopnfsup  11891  icopnfsup  11892  expeq0  12099  repswswrd  12667  repswcshw  12691  vdwlem6  14506  lublecllem  15735  tsrlemax  15967  ocv2ss  18795  0top  19570  neindisj2  19710  lmconst  19848  cnpresti  19875  sslm  19886  cmpfi  19994  dfcon2  20005  hausflim  20567  bndth  21543  nmoleub2a  21685  nmoleub2b  21686  cmetcaulem  21812  ioorf  22067  ioorinv2  22069  dgrcolem2  22756  plydiveu  22779  dvloglem  23116  lmieu  24270  axcontlem4  24391  grponnncan2  25373  dipsubdir  25880  idinside  29887  endofsegid  29888  meran1  30029  onsuct0  30059  ftc1anclem7  30262  nn0prpwlem  30306  nn0prpw  30307  fdc1  30405  rngosubdi  30522  rngosubdir  30523  mpt2bi123f  30737  ioossioc  31690  ioossioobi  31723  stoweidlem27  31975  stoweidlem31  31979  stoweidlem60  32008  atbiffatnnb  32274  3ornot23  33611  rspsbc2  33641  sbcim2g  33645  idn2  33739  idn3  33741  trsspwALT2  33957  sspwtrALT  33960  sstrALT2  33981  bj-sngltag  34889  lkreqN  35308  cdlemg33a  36845  mapdordlem2  37777
  Copyright terms: Public domain W3C validator