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