dn Show Code edit
thm (dn () () (-> (-. (-. ph)) ph)
(-> ps ps) ph a3dup himp1i com12 hid)
(-> (-. (-. ph)) ph)
edit