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

Theorem idd 21
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 19 . 2  |-  ( ps 
->  ps )
21a1i 10 1  |-  ( ph  ->  ( ps  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim1d  69  simprim  142  pm2.6  162  pm2.65  164  orel2  372  pm2.621  397  simpr  447  ancld  536  ancrd  537  anim12d  546  anim1d  547  anim2d  548  pm2.63  763  orim1d  812  orim2d  813  ecase2d  906  cad0  1390  merco2  1491  spnfw  1641  19.2  1672  r19.36av  2689  r19.44av  2697  r19.45av  2698  eqsbc3r  3049  reuss  3450  opthpr  3791  wereu2  4389  relop  4833  soxp  6190  omopth2  6578  swoord2  6686  mapdom2  7028  en3lplem2  7413  rankxplim3  7547  cfsmolem  7892  fin1a2s  8036  fpwwe2lem12  8259  fpwwe2lem13  8260  inawina  8308  gchina  8317  elnnz  10030  xmullem  10580  ioopnfsup  10964  icopnfsup  10965  expeq0  11128  vdwlem6  13029  lubid  14112  tsrlemax  14325  ocv2ss  16569  0top  16717  neindisj2  16856  lmconst  16987  cnpresti  17012  sslm  17023  cmpfi  17131  dfcon2  17141  hausflim  17672  bndth  18452  nmoleub2a  18594  nmoleub2b  18595  cmetcaulem  18710  ioorf  18924  ioorinv2  18926  itg2mulclem  19097  itg2mulc  19098  dgrcolem2  19651  plydiveu  19674  psercnlem2  19796  dvloglem  19991  grponnncan2  20915  dipsubdir  21420  axcontlem4  24005  idinside  24117  endofsegid  24118  meran1  24260  onsuct0  24290  svs2  24898  bwt2  25003  lineval5a  25499  lineval6a  25500  isconcl5a  25512  isconcl5ab  25513  nn0prpwlem  25649  nn0prpw  25650  fdc1  25867  rngosubdi  25995  rngosubdir  25996  rfcnnnub  27118  stoweidlem27  27187  stoweidlem31  27191  stoweidlem35  27195  stoweidlem60  27220  atbiffatnnb  27272  3ornot23  27553  rspsbc2  27580  sbcim2g  27585  idn2  27665  idn3  27667  trsspwALT2  27873  sspwtrALT  27876  sstrALT2  27891  lkreqN  28639  cdlemg33a  30174  mapdordlem2  31106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator