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