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

Theorem nsyl 591
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 589 . 2 (𝜒 → ¬ 𝜑)
43con2i 590 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 577  ax-in2 578
This theorem is referenced by:  con3i  595  pm4.52im  837  intnand  874  intnanrd  875  camestres  2048  camestros  2052  calemes  2059  calemos  2062  unssin  3221  inssun  3222  onsucelsucexmid  4309  funun  5011  pwuninel2  5979  swoer  6250  swoord1  6251  swoord2  6252  ssfirab  6568  djune  6676  elnnz  8656  lbioog  9226  ubioog  9227  fzneuz  9408  fzodisj  9478  fxnn0nninf  9733  infssuzex  10725
  Copyright terms: Public domain W3C validator