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