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