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