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