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