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 615 | . 2 ⊢ (𝜒 → ¬ 𝜑) |
4 | 3 | con2i 616 | 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 603 ax-in2 604 |
This theorem is referenced by: con3i 621 pm4.52im 739 intnand 916 intnanrd 917 camestres 2104 camestros 2108 calemes 2115 calemos 2118 unssin 3315 inssun 3316 onsucelsucexmid 4445 funun 5167 pwuninel2 6179 swoer 6457 swoord1 6458 swoord2 6459 ssfirab 6822 djune 6963 exmidaclem 7064 elnnz 9064 lbioog 9696 ubioog 9697 fzneuz 9881 fzodisj 9955 fxnn0nninf 10211 zfz1isolemiso 10582 infssuzex 11642 exmidunben 11939 |
Copyright terms: Public domain | W3C validator |