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