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