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