mpdan Show Code edit
# An inference based on modus ponens.
## Modus Ponens
thm (mpdan () (mpdan.1 (-> ph ps) mpdan.2 (-> (/\ ph ps) ch)) (-> ph ch) mpdan.1 mpdan.2 ex mpd)
(-> ph ch)
edit