adantr Show Code edit
## Add Conjunct
##
## (-> ph ] [ [ [ ps)
## (-> (/\ ph ] [ ch ] ) [ ps)
##
thm (adantr () (adantr.1 (-> ph ps)) (-> (/\ ph ch) ps) adantr.1 ch a1d imp)
(-> (/\ ph ch) ps)
edit