pm2.61ian Show Code edit
## Eliminate Antecedent by Cases
thm (pm2.61ian () (pm2.61ian.1 (-> (/\ ph ps) ch) pm2.61ian.2 (-> (/\ (-. ph) ps) ch)) (-> ps ch) pm2.61ian.1 ex pm2.61ian.2 ex pm2.61i)
(-> ps ch)
edit