MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  idd 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  1406  merco2  1507  spnfw  1678  19.2OLD  1709  r19.36av  2816  r19.44av  2824  r19.45av  2825  eqsbc3r  3178  reuss  3582  opthpr  3936  wereu2  4539  relop  4982  soxp  6418  omopth2  6786  swoord2  6894  mapdom2  7237  en3lplem2  7627  rankxplim3  7761  cfsmolem  8106  fin1a2s  8250  fpwwe2lem12  8472  fpwwe2lem13  8473  inawina  8521  gchina  8530  elnnz  10248  xmullem  10799  ioopnfsup  11200  icopnfsup  11201  expeq0  11365  vdwlem6  13309  lubid  14394  tsrlemax  14607  ocv2ss  16855  0top  17003  neindisj2  17142  lmconst  17279  cnpresti  17306  sslm  17317  cmpfi  17425  dfcon2  17435  hausflim  17966  bndth  18936  nmoleub2a  19078  nmoleub2b  19079  cmetcaulem  19194  ioorf  19418  ioorinv2  19420  itg2mulclem  19591  itg2mulc  19592  dgrcolem2  20145  plydiveu  20168  psercnlem2  20293  dvloglem  20492  grponnncan2  21795  dipsubdir  22302  icossicc  24082  iocssicc  24083  ioossico  24084  axcontlem4  25810  idinside  25922  endofsegid  25923  meran1  26065  onsuct0  26095  nn0prpwlem  26215  nn0prpw  26216  fdc1  26340  rngosubdi  26459  rngosubdir  26460  stoweidlem27  27643  stoweidlem31  27647  stoweidlem35  27651  stoweidlem60  27676  atbiffatnnb  27748  usgfiregdegfi  28091  3ornot23  28302  rspsbc2  28329  sbcim2g  28334  idn2  28423  idn3  28425  trsspwALT2  28641  sspwtrALT  28644  sstrALT2  28656  lkreqN  29653  cdlemg33a  31188  mapdordlem2  32120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator