nimp1i Show Code edit
thm (nimp1i () (1 (-. (-> ph ps))) ph
1 ph ps nimp1 ax-mp)
ph
edit