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