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  1642  19.2  1673  r19.36av  2690  r19.44av  2698  r19.45av  2699  eqsbc3r  3050  reuss  3451  opthpr  3792  wereu2  4392  relop  4836  soxp  6230  omopth2  6584  swoord2  6692  mapdom2  7034  en3lplem2  7419  rankxplim3  7553  cfsmolem  7898  fin1a2s  8042  fpwwe2lem12  8265  fpwwe2lem13  8266  inawina  8314  gchina  8323  elnnz  10036  xmullem  10586  ioopnfsup  10970  icopnfsup  10971  expeq0  11134  vdwlem6  13035  lubid  14118  tsrlemax  14331  ocv2ss  16575  0top  16723  neindisj2  16862  lmconst  16993  cnpresti  17018  sslm  17029  cmpfi  17137  dfcon2  17147  hausflim  17678  bndth  18458  nmoleub2a  18600  nmoleub2b  18601  cmetcaulem  18716  ioorf  18930  ioorinv2  18932  itg2mulclem  19103  itg2mulc  19104  dgrcolem2  19657  plydiveu  19680  psercnlem2  19802  dvloglem  19997  grponnncan2  20923  dipsubdir  21428  icossicc  23260  iocssicc  23261  ioossico  23262  axcontlem4  24597  idinside  24709  endofsegid  24710  meran1  24852  onsuct0  24882  itg2addnc  24935  svs2  25498  bwt2  25603  lineval5a  26099  lineval6a  26100  isconcl5a  26112  isconcl5ab  26113  nn0prpwlem  26249  nn0prpw  26250  fdc1  26467  rngosubdi  26595  rngosubdir  26596  rfcnnnub  27718  stoweidlem27  27787  stoweidlem31  27791  stoweidlem35  27795  stoweidlem60  27820  atbiffatnnb  27892  3ornot23  28326  rspsbc2  28353  sbcim2g  28358  idn2  28447  idn3  28449  trsspwALT2  28666  sspwtrALT  28669  sstrALT2  28684  lkreqN  29433  cdlemg33a  30968  mapdordlem2  31900
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator