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

Theorem pm2.61d2 152
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 10 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 pm2.61d2.1 . 2  |-  ( ph  ->  ( -.  ps  ->  ch ) )
42, 3pm2.61d 150 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.61ii  157  jaoi  368  dvelimv  1879  nfald2  1912  nfsb4t  2020  nfsbd  2050  nfabd2  2437  tfinds  4650  relimasn  5036  curry1val  6211  curry2val  6215  nfriotad  6313  riotaprc  6342  onfununi  6358  findcard2s  7099  xpfi  7128  fiint  7133  acndom  7678  dfac12k  7773  iundom2g  8162  axpowndlem3  8221  nqereu  8553  ltapr  8669  xrmax1  10504  xrmin2  10507  max1ALT  10515  hasheq0  11353  bezout  12721  ptbasfi  17276  filcon  17578  pcopt  18520  ioorinv  18931  itg1addlem2  19052  itg1addlem4  19054  itgss  19166  bddmulibl  19193  mdsymlem6  22988  sumdmdlem2  22999  ax10lem17ALT  29123  ax9lem17  29156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator