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