![]() |
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 598 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | con2i 599 |
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 586 ax-in2 587 |
This theorem is referenced by: con3i 604 jcn 624 pm4.52im 722 intnand 899 intnanrd 900 camestres 2080 camestros 2084 calemes 2091 calemos 2094 unssin 3281 inssun 3282 onsucelsucexmid 4405 funun 5125 pwuninel2 6133 swoer 6411 swoord1 6412 swoord2 6413 ssfirab 6774 djune 6915 exmidaclem 7012 elnnz 8965 lbioog 9586 ubioog 9587 fzneuz 9771 fzodisj 9845 fxnn0nninf 10101 zfz1isolemiso 10472 infssuzex 11487 exmidunben 11781 |
Copyright terms: Public domain | W3C validator |