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  562  pm4.52im  803  intnand  840  intnanrd  841  camestres  2005  camestros  2009  calemes  2016  calemos  2019  pssn2lp  3045  unssin  3176  inssun  3177  onsucelsucexmid  4255  funun  4944  pwuninel2  5897  swoer  6134  swoord1  6135  swoord2  6136  elnnz  8255  lbioog  8782  ubioog  8783  fzneuz  8963  fzodisj  9034
 Copyright terms: Public domain W3C validator