dnri Show Code edit
thm (dnri () (1 ph) (-. (-. ph))
1 ph dnr ax-mp)
(-. (-. ph))
edit