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  1658  19.2OLD  1686  r19.36av  2701  r19.44av  2709  r19.45av  2710  eqsbc3r  3061  reuss  3462  opthpr  3806  wereu2  4406  relop  4850  soxp  6244  omopth2  6598  swoord2  6706  mapdom2  7048  en3lplem2  7433  rankxplim3  7567  cfsmolem  7912  fin1a2s  8056  fpwwe2lem12  8279  fpwwe2lem13  8280  inawina  8328  gchina  8337  elnnz  10050  xmullem  10600  ioopnfsup  10984  icopnfsup  10985  expeq0  11148  vdwlem6  13049  lubid  14132  tsrlemax  14345  ocv2ss  16589  0top  16737  neindisj2  16876  lmconst  17007  cnpresti  17032  sslm  17043  cmpfi  17151  dfcon2  17161  hausflim  17692  bndth  18472  nmoleub2a  18614  nmoleub2b  18615  cmetcaulem  18730  ioorf  18944  ioorinv2  18946  itg2mulclem  19117  itg2mulc  19118  dgrcolem2  19671  plydiveu  19694  psercnlem2  19816  dvloglem  20011  grponnncan2  20937  dipsubdir  21442  icossicc  23273  iocssicc  23274  ioossico  23275  axcontlem4  24667  idinside  24779  endofsegid  24780  meran1  24922  onsuct0  24952  itg2addnc  25005  svs2  25590  bwt2  25695  lineval5a  26191  lineval6a  26192  isconcl5a  26204  isconcl5ab  26205  nn0prpwlem  26341  nn0prpw  26342  fdc1  26559  rngosubdi  26687  rngosubdir  26688  rfcnnnub  27810  stoweidlem27  27879  stoweidlem31  27883  stoweidlem35  27887  stoweidlem60  27912  atbiffatnnb  27984  3ornot23  28569  rspsbc2  28596  sbcim2g  28601  idn2  28690  idn3  28692  trsspwALT2  28909  sspwtrALT  28912  sstrALT2  28927  lkreqN  29982  cdlemg33a  31517  mapdordlem2  32449
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator