dnd Show Code edit
thm (dnd () (1 (-> ph (-. (-. ps)))) (-> ph ps)
1 ps dn syl)
(-> ph ps)
edit