nimp1 Show Code edit
thm (nimp1 () () (-> (-. (-> ph ps)) ph)
ph ps pm2.21 con1i)
(-> (-. (-> ph ps)) ph)
edit