Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nsyl Structured version   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  4214  funun  4885  pwuninel2  5835  swoer  6063  swoord1  6064  swoord2  6065  elnnz  7981  lbioog  8500  ubioog  8501  fzneuz  8679  fzodisj  8750
 Copyright terms: Public domain W3C validator