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  1892  nfald2  1925  nfsb4t  2033  nfsbd  2063  nfabd2  2450  tfinds  4666  relimasn  5052  curry1val  6227  curry2val  6231  nfriotad  6329  riotaprc  6358  onfununi  6374  findcard2s  7115  xpfi  7144  fiint  7149  acndom  7694  dfac12k  7789  iundom2g  8178  axpowndlem3  8237  nqereu  8569  ltapr  8685  xrmax1  10520  xrmin2  10523  max1ALT  10531  hasheq0  11369  bezout  12737  ptbasfi  17292  filcon  17594  pcopt  18536  ioorinv  18947  itg1addlem2  19068  itg1addlem4  19070  itgss  19182  bddmulibl  19209  mdsymlem6  23004  sumdmdlem2  23015  wlkdvspthlem  28365  dvelimvNEW7  29439  nfsb4twAUX7  29551  nfald2OLD7  29671  nfsb4tOLD7  29699  nfsb4tw2AUXOLD7  29700  nfsbdOLD7  29704  ax10lem17ALT  29745  ax9lem17  29778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator