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