ad2antrr Show Code edit
# Deduction adding conjuncts to antecedent.
## Add Conjuncts
thm (ad2antrr () (ad2ant.1 (-> ph ps)) (-> (/\ (/\ ph ch) th) ps) ad2ant.1 ch adantr th adantr)
(-> (/\ (/\ ph ch) th) ps)
edit