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