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

Theorem nsyl 600
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 598 . 2  |-  ( ch 
->  -.  ph )
43con2i 599 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 586  ax-in2 587
This theorem is referenced by:  con3i  604  jcn  624  pm4.52im  722  intnand  899  intnanrd  900  camestres  2080  camestros  2084  calemes  2091  calemos  2094  unssin  3281  inssun  3282  onsucelsucexmid  4405  funun  5125  pwuninel2  6133  swoer  6411  swoord1  6412  swoord2  6413  ssfirab  6774  djune  6915  exmidaclem  7012  elnnz  8965  lbioog  9586  ubioog  9587  fzneuz  9771  fzodisj  9845  fxnn0nninf  10101  zfz1isolemiso  10472  infssuzex  11487  exmidunben  11781
  Copyright terms: Public domain W3C validator