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

Theorem nsyl 546
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 544 . 2 (χ → ¬ φ)
43con2i 545 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 532  ax-in2 533
This theorem is referenced by:  con3i  549  pm4.52im  796  intnand  828  intnanrd  829  camestres  1987  camestros  1991  calemes  1998  calemos  2001  pssn2lp  3022  unssin  3153  inssun  3154  onsucelsucexmid  4199  funun  4870  pwuninel2  5819  swoer  6045  swoord1  6046  swoord2  6047
  Copyright terms: Public domain W3C validator