and Show Code edit
## Join consequents
thm (and () () (-> ph (-> ps (/\ ph ps)))
ph ps preand ph ps df-and-2 syl6)
(-> ph (-> ps (/\ ph ps)))
edit