anabss3 Show Code edit
## Absorb antecedent into conjunction
thm (anabss3 () (anabss3.1 (-> (/\ (/\ ph ps) ps) ch)) (-> (/\ ph ps) ch) anabss3.1 ph adantrl anidms)
(-> (/\ ph ps) ch)
edit