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