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