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  837  orim2d  838  ecase2d  938  cad0  1452  merco2  1553  spnfw  1734  r19.36av  3009  r19.44av  3018  r19.45av  3019  eqsbc3r  3393  reuss  3779  opthpr  4204  wereu2  4876  relop  5153  soxp  6896  omopth2  7233  swoord2  7341  mapdom2  7688  en3lplem2  8032  rankxplim3  8299  cfsmolem  8650  fin1a2s  8794  fpwwe2lem12  9019  fpwwe2lem13  9020  inawina  9068  gchina  9077  elnnz  10874  xmullem  11456  icossicc  11611  iocssicc  11612  ioossico  11613  ioopnfsup  11959  icopnfsup  11960  expeq0  12164  repswswrd  12719  repswcshw  12743  vdwlem6  14363  lublecllem  15475  tsrlemax  15707  ocv2ss  18499  0top  19279  neindisj2  19418  lmconst  19556  cnpresti  19583  sslm  19594  cmpfi  19702  bwthOLD  19705  dfcon2  19714  hausflim  20245  bndth  21221  nmoleub2a  21363  nmoleub2b  21364  cmetcaulem  21490  ioorf  21745  ioorinv2  21747  itg2mulclem  21916  itg2mulc  21917  dgrcolem2  22433  plydiveu  22456  psercnlem2  22581  dvloglem  22785  lmieu  23855  axcontlem4  23974  usgfiregdegfi  24615  grponnncan2  24960  dipsubdir  25467  idinside  29339  endofsegid  29340  meran1  29481  onsuct0  29511  ftc1anclem7  29701  nn0prpwlem  29745  nn0prpw  29746  fdc1  29870  rngosubdi  29987  rngosubdir  29988  mpt2bi123f  30203  ioossioc  31116  ioossioobi  31149  stoweidlem27  31355  stoweidlem31  31359  stoweidlem60  31388  atbiffatnnb  31603  3ornot23  32375  rspsbc2  32402  sbcim2g  32407  idn2  32497  idn3  32499  trsspwALT2  32715  sspwtrALT  32718  sstrALT2  32733  bj-sngltag  33640  lkreqN  33985  cdlemg33a  35520  mapdordlem2  36452
  Copyright terms: Public domain W3C validator