and2d Show Code edit
## Eliminate Conjunct
thm (and2d () (1 (-> ph (/\ ps ch))) (-> ph ch)
1 ps ch and2 syl)
(-> ph ch)
edit