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

Theorem nsyli 136
Description: A negated syllogism inference. (Contributed by NM, 3-May-1994.)
Hypotheses
Ref Expression
nsyli.1  |-  ( ph  ->  ( ps  ->  ch ) )
nsyli.2  |-  ( th 
->  -.  ch )
Assertion
Ref Expression
nsyli  |-  ( ph  ->  ( th  ->  -.  ps ) )

Proof of Theorem nsyli
StepHypRef Expression
1 nsyli.2 . 2  |-  ( th 
->  -.  ch )
2 nsyli.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
32con3d 128 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
41, 3syl5 31 1  |-  ( ph  ->  ( th  ->  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  spimehOLD  1841  tz7.7  4610  tz7.48-2  6702  tz7.49  6705  php  7294  nndomo  7303  elirrv  7568  setind  7676  zorn2lem3  8383  alephval2  8452  inar1  8655  dfon2lem6  25420  sltres  25624  onint1  26204  finminlem  26335
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator