impt Show Code edit
## Importation theorem
##
## This is the same as the import theorem, but uses the primitive
## connectives → and ¬ instead of conjunction.
##
thm (impt () () (-> (-> ph (-> ps ch)) (-> (-. (-> ph (-. ps))) ch))
ph ps preand2 ch imim1i ph imim2i
(-> (-> ph (-> ps ch)) (-> ph (-> (-. (-> ph (-. ps))) ch)))
ph ps preand1
(-> (-. (-> ph (-. ps))) ph)
syl5 pm2.43d)
(-> (-> ph (-> ps ch)) (-> (-. (-> ph (-. ps))) ch))
edit