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

Theorem nsyl 558
 Description: A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.)
Hypotheses
Ref Expression
nsyl.1 (φ → ¬ ψ)
nsyl.2 (χψ)
Assertion
Ref Expression
nsyl (φ → ¬ χ)

Proof of Theorem nsyl
StepHypRef Expression
1 nsyl.1 . . 3 (φ → ¬ ψ)
2 nsyl.2 . . 3 (χψ)
31, 2nsyl3 556 . 2 (χ → ¬ φ)
43con2i 557 1 (φ → ¬ χ)
 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 544  ax-in2 545 This theorem is referenced by:  con3i  561  pm4.52im  802  intnand  839  intnanrd  840  camestres  2002  camestros  2006  calemes  2013  calemos  2016  pssn2lp  3039  unssin  3170  inssun  3171  onsucelsucexmid  4215  funun  4887  pwuninel2  5838  swoer  6070  swoord1  6071  swoord2  6072  elnnz  8031  lbioog  8552  ubioog  8553  fzneuz  8733  fzodisj  8804
 Copyright terms: Public domain W3C validator