![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nsyl | GIF 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 626 | . 2 ⊢ (𝜒 → ¬ 𝜑) |
4 | 3 | con2i 627 | 1 ⊢ (𝜑 → ¬ 𝜒) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-in1 614 ax-in2 615 |
This theorem is referenced by: con3i 632 pm4.52im 750 intnand 931 intnanrd 932 camestres 2131 camestros 2135 calemes 2142 calemos 2145 unssin 3374 inssun 3375 onsucelsucexmid 4525 funun 5255 pwuninel2 6276 swoer 6556 swoord1 6557 swoord2 6558 ssfirab 6926 djune 7070 exmidaclem 7200 sucpw1nss3 7227 onntri35 7229 onntri45 7233 elnnz 9239 lbioog 9887 ubioog 9888 fzneuz 10074 fzodisj 10151 fxnn0nninf 10411 zfz1isolemiso 10790 infssuzex 11920 infpnlem1 12327 exmidunben 12397 lgsdir2lem2 14063 |
Copyright terms: Public domain | W3C validator |