Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nsyl | Unicode version |
Description: A negated syllogism inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 2-Mar-2013.) |
Ref | Expression |
---|---|
nsyl.1 | |
nsyl.2 |
Ref | Expression |
---|---|
nsyl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nsyl.1 | . . 3 | |
2 | nsyl.2 | . . 3 | |
3 | 1, 2 | nsyl3 588 | . 2 |
4 | 3 | con2i 589 | 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 576 ax-in2 577 |
This theorem is referenced by: con3i 594 pm4.52im 836 intnand 873 intnanrd 874 camestres 2046 camestros 2050 calemes 2057 calemos 2060 unssin 3203 inssun 3204 onsucelsucexmid 4273 funun 4964 pwuninel2 5920 swoer 6157 swoord1 6158 swoord2 6159 elnnz 8361 lbioog 8936 ubioog 8937 fzneuz 9118 fzodisj 9187 infssuzex 10345 |
Copyright terms: Public domain | W3C validator |