anim1d Show Code edit
# Add a conjunct to right of antecedent and consequent in a deduction.
## Add a conjunct to antecedent and consequent
thm (anim1d () (anim1d.1 (-> ph (-> ps ch))) (-> ph (-> (/\ ps th) (/\ ch th))) anim1d.1 ph th idd anim12d)
(-> ph (-> (/\ ps th) (/\ ch th)))
edit