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