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