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  24666  idinside  24778  endofsegid  24779  meran1  24921  onsuct0  24951  itg2addnc  25004  svs2  25589  bwt2  25694  lineval5a  26190  lineval6a  26191  isconcl5a  26203  isconcl5ab  26204  nn0prpwlem  26340  nn0prpw  26341  fdc1  26558  rngosubdi  26686  rngosubdir  26687  rfcnnnub  27809  stoweidlem27  27878  stoweidlem31  27882  stoweidlem35  27886  stoweidlem60  27911  atbiffatnnb  27983  3ornot23  28568  rspsbc2  28595  sbcim2g  28600  idn2  28689  idn3  28691  trsspwALT2  28908  sspwtrALT  28911  sstrALT2  28926  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