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