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