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