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

Theorem nsyl 629
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 627 . 2  |-  ( ch 
->  -.  ph )
43con2i 628 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 615  ax-in2 616
This theorem is referenced by:  con3i  633  pm4.52im  751  intnand  932  intnanrd  933  camestres  2143  camestros  2147  calemes  2154  calemos  2157  unssin  3389  inssun  3390  onsucelsucexmid  4547  funun  5279  pwuninel2  6308  swoer  6588  swoord1  6589  swoord2  6590  ssfirab  6963  djune  7108  exmidaclem  7238  sucpw1nss3  7265  onntri35  7267  onntri45  7271  elnnz  9294  lbioog  9945  ubioog  9946  fzneuz  10133  fzodisj  10210  fxnn0nninf  10471  zfz1isolemiso  10854  infssuzex  11985  infpnlem1  12394  exmidunben  12480  lgsdir2lem2  14908
  Copyright terms: Public domain W3C validator