preand2 Show Code edit
## Simplification
##
## This is the same as pm3.27, but uses the primitive
## connectives → and ¬ instead of conjunction. This is exactly the same as
## pm3.27im
##
thm (preand2 () () (-> (-. (-> ph (-. ps))) ps)
ph (-. ps) nimp2 ps dn syl)
(-> (-. (-> ph (-. ps))) ps)
edit