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

Theorem nsyl 617
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 615 . 2  |-  ( ch 
->  -.  ph )
43con2i 616 1  |-  ( ph  ->  -.  ch )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 603  ax-in2 604
This theorem is referenced by:  con3i  621  pm4.52im  739  intnand  916  intnanrd  917  camestres  2104  camestros  2108  calemes  2115  calemos  2118  unssin  3315  inssun  3316  onsucelsucexmid  4448  funun  5170  pwuninel2  6182  swoer  6460  swoord1  6461  swoord2  6462  ssfirab  6825  djune  6966  exmidaclem  7076  elnnz  9083  lbioog  9719  ubioog  9720  fzneuz  9905  fzodisj  9979  fxnn0nninf  10235  zfz1isolemiso  10606  infssuzex  11665  exmidunben  11962
  Copyright terms: Public domain W3C validator