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

Theorem nsyl 593
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 591 . 2  |-  ( ch 
->  -.  ph )
43con2i 592 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 579  ax-in2 580
This theorem is referenced by:  con3i  597  pm4.52im  841  intnand  878  intnanrd  879  camestres  2053  camestros  2057  calemes  2064  calemos  2067  unssin  3238  inssun  3239  onsucelsucexmid  4346  funun  5058  pwuninel2  6047  swoer  6318  swoord1  6319  swoord2  6320  ssfirab  6641  djune  6767  elnnz  8758  lbioog  9329  ubioog  9330  fzneuz  9511  fzodisj  9585  fxnn0nninf  9840  zfz1isolemiso  10240  infssuzex  11219
  Copyright terms: Public domain W3C validator