preand Show Code edit
## Join antecedents
##
## This is the same as pm3.2im, but uses the primitive
## connectives → and ¬ instead of conjunction. This is exactly the same as
## pm3.2im
##
thm (preand () () (-> ph (-> ps (-. (-> ph (-. ps)))))
ph (-. ps) nimp ps dnr syl5)
(-> ph (-> ps (-. (-> ph (-. ps)))))
edit