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

Theorem nsyl 628
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 626 . 2 (𝜒 → ¬ 𝜑)
43con2i 627 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 614  ax-in2 615
This theorem is referenced by:  con3i  632  pm4.52im  750  intnand  931  intnanrd  932  camestres  2131  camestros  2135  calemes  2142  calemos  2145  unssin  3374  inssun  3375  onsucelsucexmid  4525  funun  5255  pwuninel2  6276  swoer  6556  swoord1  6557  swoord2  6558  ssfirab  6926  djune  7070  exmidaclem  7200  sucpw1nss3  7227  onntri35  7229  onntri45  7233  elnnz  9239  lbioog  9887  ubioog  9888  fzneuz  10074  fzodisj  10151  fxnn0nninf  10411  zfz1isolemiso  10790  infssuzex  11920  infpnlem1  12327  exmidunben  12397  lgsdir2lem2  14063
  Copyright terms: Public domain W3C validator