pm2.61 Show Code edit
# a.k.a cases
## Proof by cases
thm (pm2.61 () () (-> (-> ph ps) (-> (-> (-. ph) ps) ps))
ph ps ps nsyl4t ps pm2.18 syl6)
(-> (-> ph ps) (-> (-> (-. ph) ps) ps))
edit