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  383  pm2.621  408  simpr  461  ancld  553  ancrd  554  anim12d  563  anim1d  564  anim2d  565  pm2.63  788  orim1d  839  orim2d  840  ecase2d  940  cad0  1455  merco2  1556  spnfw  1771  r19.36av  2991  r19.44av  3000  r19.45av  3001  eqsbc3r  3375  reuss  3764  opthpr  4193  wereu2  4866  relop  5143  soxp  6898  omopth2  7235  swoord2  7343  mapdom2  7690  en3lplem2  8035  rankxplim3  8302  cfsmolem  8653  fin1a2s  8797  fpwwe2lem12  9022  fpwwe2lem13  9023  inawina  9071  gchina  9080  elnnz  10881  xmullem  11466  icossicc  11621  iocssicc  11622  ioossico  11623  ioopnfsup  11972  icopnfsup  11973  expeq0  12177  repswswrd  12737  repswcshw  12761  vdwlem6  14485  lublecllem  15596  tsrlemax  15828  ocv2ss  18681  0top  19462  neindisj2  19601  lmconst  19739  cnpresti  19766  sslm  19777  cmpfi  19885  bwthOLD  19888  dfcon2  19897  hausflim  20459  bndth  21435  nmoleub2a  21577  nmoleub2b  21578  cmetcaulem  21704  ioorf  21959  ioorinv2  21961  dgrcolem2  22647  plydiveu  22670  dvloglem  23005  lmieu  24126  axcontlem4  24246  grponnncan2  25232  dipsubdir  25739  idinside  29709  endofsegid  29710  meran1  29851  onsuct0  29881  ftc1anclem7  30071  nn0prpwlem  30115  nn0prpw  30116  fdc1  30214  rngosubdi  30331  rngosubdir  30332  mpt2bi123f  30546  ioossioc  31460  ioossioobi  31493  stoweidlem27  31698  stoweidlem31  31702  stoweidlem60  31731  atbiffatnnb  31946  3ornot23  33011  rspsbc2  33038  sbcim2g  33042  idn2  33132  idn3  33134  trsspwALT2  33350  sspwtrALT  33353  sstrALT2  33368  bj-sngltag  34289  lkreqN  34635  cdlemg33a  36172  mapdordlem2  37104
  Copyright terms: Public domain W3C validator