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