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