pm2.61ii Show Code edit
## Eliminate an antecedent
thm (pm2.61ii () (1 (-> (-. ph) (-> (-. ps) ch)) 2 (-> ph ch) 3 (-> ps ch)) ch
3 con3i 2 con3i 1 syl mpd pm2.18i)
ch
edit