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