ancrd Show Code edit
# Deduction conjoining antecedent to right of consequent in nested
# implication.
## Add Antecedent
thm (ancrd () (ancrd.1 (-> ph (-> ps ch))) (-> ph (-> ps (/\ ch ps))) ancrd.1 ps ch ancr syl)
(-> ph (-> ps (/\ ch ps)))
edit