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  2800  r19.44av  2808  r19.45av  2809  eqsbc3r  3162  reuss  3566  opthpr  3919  wereu2  4521  relop  4964  soxp  6396  omopth2  6764  swoord2  6872  mapdom2  7215  en3lplem2  7605  rankxplim3  7739  cfsmolem  8084  fin1a2s  8228  fpwwe2lem12  8450  fpwwe2lem13  8451  inawina  8499  gchina  8508  elnnz  10225  xmullem  10776  ioopnfsup  11173  icopnfsup  11174  expeq0  11338  vdwlem6  13282  lubid  14367  tsrlemax  14580  ocv2ss  16824  0top  16972  neindisj2  17111  lmconst  17248  cnpresti  17275  sslm  17286  cmpfi  17394  dfcon2  17404  hausflim  17935  bndth  18855  nmoleub2a  18997  nmoleub2b  18998  cmetcaulem  19113  ioorf  19333  ioorinv2  19335  itg2mulclem  19506  itg2mulc  19507  dgrcolem2  20060  plydiveu  20083  psercnlem2  20208  dvloglem  20407  grponnncan2  21691  dipsubdir  22198  icossicc  23966  iocssicc  23967  ioossico  23968  axcontlem4  25621  idinside  25733  endofsegid  25734  meran1  25876  onsuct0  25906  itg2addnc  25960  nn0prpwlem  26017  nn0prpw  26018  fdc1  26142  rngosubdi  26261  rngosubdir  26262  stoweidlem27  27445  stoweidlem31  27449  stoweidlem35  27453  stoweidlem60  27478  atbiffatnnb  27550  3ornot23  27935  rspsbc2  27962  sbcim2g  27967  idn2  28056  idn3  28058  trsspwALT2  28274  sspwtrALT  28277  sstrALT2  28289  lkreqN  29286  cdlemg33a  30821  mapdordlem2  31753
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator