pm2.43d Show Code edit
## Absorb redundant antecedent
##
## (-> ph [ (-> ps [ (-> ps ch)))
## (-> ph [ [ (-> ps ch))
##
thm (pm2.43d () (1 (-> ph (-> ps (-> ps ch)))) (-> ph (-> ps ch))
1 ps ch pm2.43 syl)
(-> ph (-> ps ch))
edit