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  1640  19.2  1671  r19.36av  2688  r19.44av  2696  r19.45av  2697  eqsbc3r  3048  reuss  3449  opthpr  3790  wereu2  4390  relop  4834  soxp  6228  omopth2  6582  swoord2  6690  mapdom2  7032  en3lplem2  7417  rankxplim3  7551  cfsmolem  7896  fin1a2s  8040  fpwwe2lem12  8263  fpwwe2lem13  8264  inawina  8312  gchina  8321  elnnz  10034  xmullem  10584  ioopnfsup  10968  icopnfsup  10969  expeq0  11132  vdwlem6  13033  lubid  14116  tsrlemax  14329  ocv2ss  16573  0top  16721  neindisj2  16860  lmconst  16991  cnpresti  17016  sslm  17027  cmpfi  17135  dfcon2  17145  hausflim  17676  bndth  18456  nmoleub2a  18598  nmoleub2b  18599  cmetcaulem  18714  ioorf  18928  ioorinv2  18930  itg2mulclem  19101  itg2mulc  19102  dgrcolem2  19655  plydiveu  19678  psercnlem2  19800  dvloglem  19995  grponnncan2  20921  dipsubdir  21426  icossicc  23258  iocssicc  23259  ioossico  23260  axcontlem4  24595  idinside  24707  endofsegid  24708  meran1  24850  onsuct0  24880  svs2  25487  bwt2  25592  lineval5a  26088  lineval6a  26089  isconcl5a  26101  isconcl5ab  26102  nn0prpwlem  26238  nn0prpw  26239  fdc1  26456  rngosubdi  26584  rngosubdir  26585  rfcnnnub  27707  stoweidlem27  27776  stoweidlem31  27780  stoweidlem35  27784  stoweidlem60  27809  atbiffatnnb  27881  3ornot23  28270  rspsbc2  28297  sbcim2g  28302  idn2  28385  idn3  28387  trsspwALT2  28593  sspwtrALT  28596  sstrALT2  28611  lkreqN  29360  cdlemg33a  30895  mapdordlem2  31827
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator