jctild Show Code edit
# Deduction conjoining a theorem to left of consequent in an
# implication.
thm (jctild () (jctild.1 (-> ph (-> ps ch)) jctild.2 (-> ph th)) (-> ph (-> ps (/\ th ch))) jctild.2 ps a1d jctild.1 jcad)
(-> ph (-> ps (/\ th ch)))
edit