df-and-2 Show Code edit
## Definition of AND Implication
thm (df-and-2 () () (-> (-. (-> ph (-. ps))) (/\ ph ps))
ph ps df-and preand2i)
(-> (-. (-> ph (-. ps))) (/\ ph ps))
edit