pm2.43a Show Code edit
## Absorb redundant antecedent
thm (pm2.43a () (1 (-> ps (-> ph (-> ps ch)))) (-> ps (-> ph ch))
1 com23 pm2.43i)
(-> ps (-> ph ch))
edit