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  1677  19.2OLD  1707  r19.36av  2799  r19.44av  2807  r19.45av  2808  eqsbc3r  3161  reuss  3565  opthpr  3918  wereu2  4520  relop  4963  soxp  6395  omopth2  6763  swoord2  6871  mapdom2  7214  en3lplem2  7604  rankxplim3  7738  cfsmolem  8083  fin1a2s  8227  fpwwe2lem12  8449  fpwwe2lem13  8450  inawina  8498  gchina  8507  elnnz  10224  xmullem  10775  ioopnfsup  11172  icopnfsup  11173  expeq0  11337  vdwlem6  13281  lubid  14366  tsrlemax  14579  ocv2ss  16823  0top  16971  neindisj2  17110  lmconst  17247  cnpresti  17274  sslm  17285  cmpfi  17393  dfcon2  17403  hausflim  17934  bndth  18854  nmoleub2a  18996  nmoleub2b  18997  cmetcaulem  19112  ioorf  19332  ioorinv2  19334  itg2mulclem  19505  itg2mulc  19506  dgrcolem2  20059  plydiveu  20082  psercnlem2  20207  dvloglem  20406  grponnncan2  21690  dipsubdir  22197  icossicc  23965  iocssicc  23966  ioossico  23967  axcontlem4  25620  idinside  25732  endofsegid  25733  meran1  25875  onsuct0  25905  itg2addnc  25959  nn0prpwlem  26016  nn0prpw  26017  fdc1  26141  rngosubdi  26260  rngosubdir  26261  stoweidlem27  27444  stoweidlem31  27448  stoweidlem35  27452  stoweidlem60  27477  atbiffatnnb  27549  3ornot23  27934  rspsbc2  27961  sbcim2g  27966  idn2  28055  idn3  28057  trsspwALT2  28273  sspwtrALT  28276  sstrALT2  28288  lkreqN  29285  cdlemg33a  30820  mapdordlem2  31752
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator