MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nsyli 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  1830  tz7.7  4541  tz7.48-2  6628  tz7.49  6631  php  7220  nndomo  7229  elirrv  7491  setind  7599  zorn2lem3  8304  alephval2  8373  inar1  8576  dfon2lem6  25161  sltres  25335  onint1  25906  finminlem  26005  ax9lem12  29127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator