nsyl Show Code edit
## Negated Syllogism
thm (nsyl () (1 (-> ph (-. ps)) 2 (-> ch ps)) (-> ph (-. ch))
1 2 con3i syl)
(-> ph (-. ch))
edit