ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nsyl Unicode version

Theorem nsyl 591
Description: A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
Hypotheses
Ref Expression
nsyl.1  |-  ( ph  ->  -.  ps )
nsyl.2  |-  ( ch 
->  ps )
Assertion
Ref Expression
nsyl  |-  ( ph  ->  -.  ch )

Proof of Theorem nsyl
StepHypRef Expression
1 nsyl.1 . . 3  |-  ( ph  ->  -.  ps )
2 nsyl.2 . . 3  |-  ( ch 
->  ps )
31, 2nsyl3 589 . 2  |-  ( ch 
->  -.  ph )
43con2i 590 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 577  ax-in2 578
This theorem is referenced by:  con3i  595  pm4.52im  837  intnand  874  intnanrd  875  camestres  2047  camestros  2051  calemes  2058  calemos  2061  unssin  3210  inssun  3211  onsucelsucexmid  4281  funun  4974  pwuninel2  5931  swoer  6200  swoord1  6201  swoord2  6202  elnnz  8442  lbioog  9012  ubioog  9013  fzneuz  9194  fzodisj  9264  infssuzex  10489
  Copyright terms: Public domain W3C validator