nimpi Show Code edit
thm (nimpi () (1 ph 2 (-. ps)) (-. (-> ph ps))
2 1 ph ps nimp ax-mp ax-mp)
(-. (-> ph ps))
edit