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