anabsi8 Show Code edit
## Absorb antecedent into conjunction
thm (anabsi8 () (anabsi8.1 (-> ps (-> (/\ ps ph) ch))) (-> (/\ ph ps) ch) anabsi8.1 anabsi5 ancoms)
(-> (/\ ph ps) ch)
edit