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  2792  r19.44av  2800  r19.45av  2801  eqsbc3r  3154  reuss  3558  opthpr  3911  wereu2  4513  relop  4956  soxp  6388  omopth2  6756  swoord2  6864  mapdom2  7207  en3lplem2  7597  rankxplim3  7731  cfsmolem  8076  fin1a2s  8220  fpwwe2lem12  8442  fpwwe2lem13  8443  inawina  8491  gchina  8500  elnnz  10217  xmullem  10768  ioopnfsup  11165  icopnfsup  11166  expeq0  11330  vdwlem6  13274  lubid  14359  tsrlemax  14572  ocv2ss  16816  0top  16964  neindisj2  17103  lmconst  17240  cnpresti  17267  sslm  17278  cmpfi  17386  dfcon2  17396  hausflim  17927  bndth  18847  nmoleub2a  18989  nmoleub2b  18990  cmetcaulem  19105  ioorf  19325  ioorinv2  19327  itg2mulclem  19498  itg2mulc  19499  dgrcolem2  20052  plydiveu  20075  psercnlem2  20200  dvloglem  20399  grponnncan2  21683  dipsubdir  22190  icossicc  23958  iocssicc  23959  ioossico  23960  axcontlem4  25613  idinside  25725  endofsegid  25726  meran1  25868  onsuct0  25898  itg2addnc  25952  nn0prpwlem  26009  nn0prpw  26010  fdc1  26134  rngosubdi  26253  rngosubdir  26254  stoweidlem27  27437  stoweidlem31  27441  stoweidlem35  27445  stoweidlem60  27470  atbiffatnnb  27542  3ornot23  27927  rspsbc2  27954  sbcim2g  27959  idn2  28048  idn3  28050  trsspwALT2  28266  sspwtrALT  28269  sstrALT2  28281  lkreqN  29336  cdlemg33a  30871  mapdordlem2  31803
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator