anabsi7 Show Code edit
## Absorb antecedent into conjunction
thm (anabsi7 () (anabsi7.1 (-> ps (-> (/\ ph ps) ch))) (-> (/\ ph ps) ch) anabsi7.1 exp3a pm2.43b imp)
(-> (/\ ph ps) ch)
edit