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  1734  tz7.7  4434  tz7.48-2  6470  tz7.49  6473  php  7061  nndomo  7070  elirrv  7327  setind  7435  zorn2lem3  8141  alephval2  8210  inar1  8413  dfon2lem6  24215  sltres  24389  onint1  24960  finminlem  26334  ax9lem12  29773
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator