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