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

Theorem nsyl 618
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 616 . 2 (𝜒 → ¬ 𝜑)
43con2i 617 1 (𝜑 → ¬ 𝜒)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 604  ax-in2 605
This theorem is referenced by:  con3i  622  pm4.52im  740  intnand  917  intnanrd  918  camestres  2105  camestros  2109  calemes  2116  calemos  2119  unssin  3319  inssun  3320  onsucelsucexmid  4452  funun  5174  pwuninel2  6186  swoer  6464  swoord1  6465  swoord2  6466  ssfirab  6829  djune  6970  exmidaclem  7080  elnnz  9087  lbioog  9725  ubioog  9726  fzneuz  9911  fzodisj  9985  fxnn0nninf  10241  zfz1isolemiso  10613  infssuzex  11676  exmidunben  11973
  Copyright terms: Public domain W3C validator