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