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

Theorem nsyli 135
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 127 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
41, 3syl5 30 1  |-  ( ph  ->  ( th  ->  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  spimehOLD  1840  tz7.7  4599  tz7.48-2  6691  tz7.49  6694  php  7283  nndomo  7292  elirrv  7557  setind  7665  zorn2lem3  8370  alephval2  8439  inar1  8642  dfon2lem6  25407  sltres  25611  onint1  26191  finminlem  26312
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator