New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE 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 111 | . 2 ⊢ (χ → ¬ φ) |
4 | 3 | con2i 112 | 1 ⊢ (φ → ¬ χ) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem is referenced by: con3i 127 intnand 882 intnanrd 883 ax12 1935 ax6 2147 ax12from12o 2156 camestres 2308 camestros 2312 calemes 2319 calemos 2322 pssn2lp 3370 0nelsuc 4400 nnsucelr 4428 tfinltfin 4501 nnadjoin 4520 funun 5146 oprssdm 5612 |
Copyright terms: Public domain | W3C validator |