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