mpan Show Code edit
## Modus ponens
thm (mpan () (mpan.1 ph mpan.2 (-> (/\ ph ps) ch)) (-> ps ch) mpan.1 mpan.2 ex ax-mp)
(-> ps ch)
edit