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