pm2.27 Show Code edit
## Modus Ponens
##
## This theorem can be thought of as a closed form of modus ponens.
##
thm (pm2.27 () () (-> ph (-> (-> ph ps) ps))
(-> ph ps) id com12)
(-> ph (-> (-> ph ps) ps))
edit