mpani Show Code edit
# An inference based on modus ponens.
## Modus Ponens
thm (mpani () (mpani.1 ps mpani.2 (-> ph (-> (/\ ps ch) th))) (-> ph (-> ch th)) mpani.1 mpani.2 exp3a mpi)
(-> ph (-> ch th))
edit