anim12d Show Code edit
# Conjoin antecedents and consequents in a deduction.
## Join antecedents and consequents
thm (anim12d () (anim12d.1 (-> ph (-> ps ch)) anim12d.2 (-> ph (-> th ta))) (-> ph (-> (/\ ps th) (/\ ch ta))) ps ch th ta prth anim12d.1 anim12d.2 sylanc)
(-> ph (-> (/\ ps th) (/\ ch ta)))
edit