![]() |
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 591 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | con2i 592 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-in1 579 ax-in2 580 |
This theorem is referenced by: con3i 597 pm4.52im 841 intnand 878 intnanrd 879 camestres 2053 camestros 2057 calemes 2064 calemos 2067 unssin 3238 inssun 3239 onsucelsucexmid 4346 funun 5058 pwuninel2 6047 swoer 6318 swoord1 6319 swoord2 6320 ssfirab 6641 djune 6767 elnnz 8758 lbioog 9329 ubioog 9330 fzneuz 9511 fzodisj 9585 fxnn0nninf 9840 zfz1isolemiso 10240 infssuzex 11219 |
Copyright terms: Public domain | W3C validator |