nimpd Show Code edit
thm (nimpd () (1 (-> ph ps) 2 (-> ph (-. ch))) (-> ph (-. (-> ps ch)))
2 1 ps ch nimp syl mpd)
(-> ph (-. (-> ps ch)))
edit