dnrd Show Code edit
thm (dnrd () (1 (-> ph ps)) (-> ph (-. (-. ps)))
1 ps dnr syl)
(-> ph (-. (-. ps)))
edit