anabsi5 Show Code edit
## Absorb conjunct
thm (anabsi5 () (anabsi5.1 (-> ph (-> (/\ ph ps) ch))) (-> (/\ ph ps) ch) anabsi5.1 ps adantr pm2.43i)
(-> (/\ ph ps) ch)
edit