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

Theorem idd 22
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 20 . 2  |-  ( ps 
->  ps )
21a1i 11 1  |-  ( ph  ->  ( ps  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim1d  71  simprim  144  pm2.6  164  pm2.65  166  orel2  373  pm2.621  398  simpr  448  ancld  537  ancrd  538  anim12d  547  anim1d  548  anim2d  549  pm2.63  764  orim1d  813  orim2d  814  ecase2d  907  cad0  1409  merco2  1510  spnfw  1682  19.2OLD  1713  r19.36av  2848  r19.44av  2856  r19.45av  2857  eqsbc3r  3210  reuss  3614  opthpr  3968  wereu2  4571  relop  5015  soxp  6451  omopth2  6819  swoord2  6927  mapdom2  7270  en3lplem2  7663  rankxplim3  7797  cfsmolem  8142  fin1a2s  8286  fpwwe2lem12  8508  fpwwe2lem13  8509  inawina  8557  gchina  8566  elnnz  10284  xmullem  10835  ioopnfsup  11237  icopnfsup  11238  expeq0  11402  vdwlem6  13346  lubid  14431  tsrlemax  14644  ocv2ss  16892  0top  17040  neindisj2  17179  lmconst  17317  cnpresti  17344  sslm  17355  cmpfi  17463  bwth  17465  dfcon2  17474  hausflim  18005  bndth  18975  nmoleub2a  19117  nmoleub2b  19118  cmetcaulem  19233  ioorf  19457  ioorinv2  19459  itg2mulclem  19630  itg2mulc  19631  dgrcolem2  20184  plydiveu  20207  psercnlem2  20332  dvloglem  20531  grponnncan2  21834  dipsubdir  22341  icossicc  24121  iocssicc  24122  ioossico  24123  axcontlem4  25898  idinside  26010  endofsegid  26011  meran1  26153  onsuct0  26183  ftc1anclem7  26276  nn0prpwlem  26316  nn0prpw  26317  fdc1  26441  rngosubdi  26560  rngosubdir  26561  stoweidlem27  27743  stoweidlem31  27747  stoweidlem35  27751  stoweidlem60  27776  atbiffatnnb  27848  usgfiregdegfi  28314  3ornot23  28528  rspsbc2  28555  sbcim2g  28560  idn2  28651  idn3  28653  trsspwALT2  28869  sspwtrALT  28872  sstrALT2  28884  lkreqN  29905  cdlemg33a  31440  mapdordlem2  32372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator