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