and1 Show Code edit
## Eliminate Conjunct
thm (and1 () () (-> (/\ ph ps) ph)
ph ps df-and-1 ph ps preand1 syl)
(-> (/\ ph ps) ph)
edit