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