mp2and Show Code edit
# A deduction based on modus ponens.
## Modus Ponens
thm (mp2and () (mp2and.1 (-> ph ps) mp2and.2 (-> ph ch) mp2and.3 (-> ph (-> (/\ ps ch) th))) (-> ph th) mp2and.2 mp2and.1 mp2and.3 mpand mpd)
(-> ph th)
edit