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  786  orim1d  835  orim2d  836  ecase2d  931  cad0  1443  merco2  1544  spnfw  1725  r19.36av  2968  r19.44av  2977  r19.45av  2978  eqsbc3r  3350  reuss  3734  opthpr  4153  wereu2  4820  relop  5093  soxp  6790  omopth2  7128  swoord2  7236  mapdom2  7587  en3lplem2  7927  rankxplim3  8194  cfsmolem  8545  fin1a2s  8689  fpwwe2lem12  8914  fpwwe2lem13  8915  inawina  8963  gchina  8972  elnnz  10762  xmullem  11333  icossicc  11488  iocssicc  11489  ioossico  11490  ioopnfsup  11815  icopnfsup  11816  expeq0  12006  repswswrd  12535  repswcshw  12559  vdwlem6  14160  lublecllem  15272  tsrlemax  15504  ocv2ss  18218  0top  18715  neindisj2  18854  lmconst  18992  cnpresti  19019  sslm  19030  cmpfi  19138  bwthOLD  19141  dfcon2  19150  hausflim  19681  bndth  20657  nmoleub2a  20799  nmoleub2b  20800  cmetcaulem  20926  ioorf  21181  ioorinv2  21183  itg2mulclem  21352  itg2mulc  21353  dgrcolem2  21869  plydiveu  21892  psercnlem2  22017  dvloglem  22221  axcontlem4  23360  grponnncan2  23888  dipsubdir  24395  idinside  28254  endofsegid  28255  meran1  28396  onsuct0  28426  ftc1anclem7  28616  nn0prpwlem  28660  nn0prpw  28661  fdc1  28785  rngosubdi  28902  rngosubdir  28903  mpt2bi123f  29118  stoweidlem27  29965  stoweidlem31  29969  stoweidlem60  29998  atbiffatnnb  30070  usgfiregdegfi  30671  3ornot23  31526  rspsbc2  31553  sbcim2g  31558  idn2  31648  idn3  31650  trsspwALT2  31866  sspwtrALT  31869  sstrALT2  31884  bj-sngltag  32789  lkreqN  33134  cdlemg33a  34669  mapdordlem2  35601
  Copyright terms: Public domain W3C validator