nimp2 Show Code edit
thm (nimp2 () () (-> (-. (-> ph ps)) (-. ps))
ps ph ax-1 con3i)
(-> (-. (-> ph ps)) (-. ps))
edit