![]() |
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 627 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | con2i 628 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 615 ax-in2 616 |
This theorem is referenced by: con3i 633 pm4.52im 751 intnand 932 intnanrd 933 camestres 2143 camestros 2147 calemes 2154 calemos 2157 unssin 3389 inssun 3390 onsucelsucexmid 4547 funun 5279 pwuninel2 6308 swoer 6588 swoord1 6589 swoord2 6590 ssfirab 6963 djune 7108 exmidaclem 7238 sucpw1nss3 7265 onntri35 7267 onntri45 7271 elnnz 9294 lbioog 9945 ubioog 9946 fzneuz 10133 fzodisj 10210 fxnn0nninf 10471 zfz1isolemiso 10854 infssuzex 11985 infpnlem1 12394 exmidunben 12480 lgsdir2lem2 14908 |
Copyright terms: Public domain | W3C validator |