mpd Show Code edit
## Modus Ponens
##
## (-> ph [ ps ] ] )
## (-> ph (-> [ ps ] [ ch))
## (-> ph [ [ [ ch)
##
thm (mpd () (1 (-> ph ps) 2 (-> ph (-> ps ch))) (-> ph ch)
1 2 a2i ax-mp)
(-> ph ch)
edit