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

Theorem pm2.61d2 160
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 158 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  165  jaoi  377  nfald2  2099  nfsbd  2210  2ax6elem  2217  sbal1  2228  sbal2  2229  nfabd2  2585  rgen2a  2830  relimasn  5301  nfriotad  6204  tfinds  6632  curry1val  6831  curry2val  6835  onfununi  6969  findcard2s  7715  xpfi  7745  fiint  7751  acndom  8384  dfac12k  8479  iundom2g  8867  nqereu  9257  ltapr  9373  xrmax1  11347  xrmin2  11350  max1ALT  11358  hasheq0  12388  swrdnd2  12621  cshw1  12753  bezout  14281  ptbasfi  20266  filcon  20568  pcopt  21706  ioorinv  22169  itg1addlem2  22288  itg1addlem4  22290  itgss  22402  bddmulibl  22429  wlkdvspthlem  24907  mdsymlem6  27620  sumdmdlem2  27631  wl-equsb4  31358  wl-sbalnae  31365  sgoldbaltlem1  37813
  Copyright terms: Public domain W3C validator