anabsi6 Show Code edit
## Absorb conjunct
thm (anabsi6 () (anabsi6.1 (-> ph (-> (/\ ps ph) ch))) (-> (/\ ph ps) ch) anabsi6.1 ancomsd anabsi5)
(-> (/\ ph ps) ch)
edit