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

Theorem nsyli 133
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 125 . 2  |-  ( ph  ->  ( -.  ch  ->  -. 
ps ) )
41, 3syl5 28 1  |-  ( ph  ->  ( th  ->  -.  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  spimeh  1722  tz7.7  4418  tz7.48-2  6454  tz7.49  6457  php  7045  nndomo  7054  elirrv  7311  setind  7419  zorn2lem3  8125  alephval2  8194  inar1  8397  dfon2lem6  23555  sltres  23729  onint1  24299  finminlem  25643  ax9lem12  28524
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator