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

Theorem pm2.61d2 154
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 152 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.61ii  159  jaoi  369  dvelimvOLD  2028  nfald2  2064  nfsb4tOLD  2128  nfsbd  2187  nfabd2  2590  tfinds  4839  relimasn  5227  curry1val  6439  curry2val  6443  nfriotad  6558  riotaprc  6587  onfununi  6603  findcard2s  7349  xpfi  7378  fiint  7383  acndom  7932  dfac12k  8027  iundom2g  8415  axpowndlem3  8474  nqereu  8806  ltapr  8922  xrmax1  10763  xrmin2  10766  max1ALT  10774  hasheq0  11644  bezout  13042  ptbasfi  17613  filcon  17915  pcopt  19047  ioorinv  19468  itg1addlem2  19589  itg1addlem4  19591  itgss  19703  bddmulibl  19730  wlkdvspthlem  21607  mdsymlem6  23911  sumdmdlem2  23922  swrdvalodm2  28188  swrdvalodm  28189  cshw1  28275  dvelimvNEW7  29462  nfsb4twAUX7  29576  nfsbdwAUX7  29578  ax7w15AUX7  29668  nfald2OLD7  29717  nfsb4tOLD7  29745  nfsb4tw2AUXOLD7  29746  nfsbdOLD7  29750
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator