anim2i Show Code edit
# Introduce conjunct to both sides of an implication.
## Introduce conjunct to both sides
thm (anim2i () (anim1i.1 (-> ph ps)) (-> (/\ ch ph) (/\ ch ps)) ch id anim1i.1 anim12i)
(-> (/\ ch ph) (/\ ch ps))
edit