MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.61d2 Structured version   Unicode version

Theorem pm2.61d2 164
Description: Inference eliminating an antecedent. (Contributed by NM, 18-Aug-1993.)
Hypotheses
Ref Expression
pm2.61d2.1  |-  ( ph  ->  ( -.  ps  ->  ch ) )
pm2.61d2.2  |-  ( ps 
->  ch )
Assertion
Ref Expression
pm2.61d2  |-  ( ph  ->  ch )

Proof of Theorem pm2.61d2
StepHypRef Expression
1 pm2.61d2.2 . . 3  |-  ( ps 
->  ch )
21a1i 11 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61d2.1 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
42, 3pm2.61d 162 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.61ii  169  jaoi  381  nfald2  2129  nfsbd  2238  2ax6elem  2245  sbal1  2256  sbal2  2257  nfabd2  2606  rgen2a  2853  relimasn  5208  nfriotad  6273  tfinds  6698  curry1val  6898  curry2val  6902  onfununi  7066  findcard2s  7816  xpfi  7846  fiint  7852  acndom  8484  dfac12k  8579  iundom2g  8967  nqereu  9356  ltapr  9472  xrmax1  11472  xrmin2  11475  max1ALT  11483  hasheq0  12545  swrdnd2  12785  cshw1  12917  bezout  14503  ptbasfi  20588  filcon  20890  pcopt  22045  ioorinv  22520  ioorinvOLD  22525  itg1addlem2  22647  itg1addlem4  22649  itgss  22761  bddmulibl  22788  wlkdvspthlem  25329  mdsymlem6  28053  sumdmdlem2  28064  wl-equsb4  31843  wl-sbalnae  31850  poimirlem13  31911  poimirlem25  31923  poimirlem27  31925  sgoldbaltlem1  38636
  Copyright terms: Public domain W3C validator