mpand Show Code edit
# A deduction based on modus ponens.
## Modus Ponens
thm (mpand () (mpand.1 (-> ph ps) mpand.2 (-> ph (-> (/\ ps ch) th))) (-> ph (-> ch th)) mpand.1 mpand.2 exp3a mpd)
(-> ph (-> ch th))
edit