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