anim12i Show Code edit
# Conjoin antecedents and consequents of two premises.
## Join antecedents and consequents
thm (anim12i () (anim12i.1 (-> ph ps) anim12i.2 (-> ch th)) (-> (/\ ph ch) (/\ ps th)) ph ch pm3.26 anim12i.1 syl ph ch pm3.27 anim12i.2 syl jca)
(-> (/\ ph ch) (/\ ps th))
edit