casesd Show Code edit
## Proof by cases
thm (casesd () (1 (-> ph (-> ps ch)) 2 (-> ph (-> (-. ps) ch))) (-> ph ch)
2 1 ps ch cases syl mpd)
(-> ph ch)
edit