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