ILE Home 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  3042  unssin  3173  inssun  3174  onsucelsucexmid  4251  funun  4931  pwuninel2  5884  swoer  6121  swoord1  6122  swoord2  6123  elnnz  8227  lbioog  8749  ubioog  8750  fzneuz  8930  fzodisj  9001
  Copyright terms: Public domain W3C validator