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