olcs Show Code edit
## Eliminate a Disjunct
thm (olcs () (hyp (-> (\/ ph ps) ch)) (-> ps ch)
ps ph olc
(-> ps (\/ ph ps))
hyp
(-> (\/ ph ps) ch)
syl
(-> ps ch)
)
edit