anabss7 Show Code edit
## Absorb antecedent into conjunction
thm (anabss7 () (anabss7.1 (-> (/\ ps (/\ ph ps)) ch)) (-> (/\ ph ps) ch) anabss7.1 ex anabsi7)
(-> (/\ ph ps) ch)
edit