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

Theorem idd 25
Description: Principle of identity id 22 with antecedent. (Contributed by NM, 26-Nov-1995.)
Assertion
Ref Expression
idd  |-  ( ph  ->  ( ps  ->  ps ) )

Proof of Theorem idd
StepHypRef Expression
1 id 22 . 2  |-  ( ps 
->  ps )
21a1i 11 1  |-  ( ph  ->  ( ps  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim1d  78  simprim  153  pm2.6  173  pm2.65  175  orel2  384  pm2.621  409  simpr  462  ancld  555  ancrd  556  anim12d  565  anim1d  566  anim2d  567  pm2.63  795  orim1d  847  orim2d  848  ecase2d  948  cad0  1513  merco2  1613  spnfw  1837  r19.36v  2915  r19.44v  2924  r19.45v  2925  eqsbc3r  3299  reuss  3697  opthpr  4121  wereu2  4793  relop  4947  soxp  6864  omopth2  7240  swoord2  7348  mapdom2  7696  en3lplem2  8073  rankxplim3  8304  cfsmolem  8651  fin1a2s  8795  fpwwe2lem12  9017  fpwwe2lem13  9018  inawina  9066  gchina  9075  elnnz  10898  xmullem  11501  icossicc  11672  iocssicc  11673  ioossico  11674  ioopnfsup  12041  icopnfsup  12042  expeq0  12252  repswswrd  12833  repswcshw  12857  coprmprod  14621  vdwlem6  14879  lublecllem  16177  tsrlemax  16409  ocv2ss  19178  0top  19941  neindisj2  20081  lmconst  20219  cnpresti  20246  sslm  20257  cmpfi  20365  dfcon2  20376  hausflim  20938  bndth  21928  nmoleub2a  22073  nmoleub2b  22074  cmetcaulem  22200  ioorf  22467  ioorinv2  22469  ioorfOLD  22472  ioorinv2OLD  22474  dgrcolem2  23170  plydiveu  23193  dvloglem  23535  lmieu  24768  axcontlem4  24939  grponnncan2  25924  dipsubdir  26431  omssubadd  29080  idinside  30800  endofsegid  30801  nn0prpwlem  30927  nn0prpw  30928  meran1  31020  onsuct0  31050  bj-sngltag  31488  poimirlem26  31873  ftc1anclem7  31930  fdc1  31982  rngosubdi  32099  rngosubdir  32100  mpt2bi123f  32313  lkreqN  32648  cdlemg33a  34185  mapdordlem2  35117  cnvtrucl0  36144  3ornot23  36778  rspsbc2  36808  sbcim2g  36812  idn2  36906  idn3  36908  trsspwALT2  37123  sspwtrALT  37126  sstrALT2  37147  ioossioc  37480  ioossioobi  37510  stoweidlem27  37770  stoweidlem31  37775  stoweidlem60  37804  hoidmvlelem3  38266  atbiffatnnb  38314  el1fzopredsuc  38535
  Copyright terms: Public domain W3C validator