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