ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nsyl Structured version   Unicode 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  561  pm4.52im  802  intnand  839  intnanrd  840  camestres  2002  camestros  2006  calemes  2013  calemos  2016  pssn2lp  3039  unssin  3170  inssun  3171  onsucelsucexmid  4215  funun  4887  pwuninel2  5838  swoer  6070  swoord1  6071  swoord2  6072  elnnz  8011  lbioog  8532  ubioog  8533  fzneuz  8713  fzodisj  8784
  Copyright terms: Public domain W3C validator