mt2d Show Code edit
## Modus Tollens
thm (mt2d () (1 (-> ph ch) 2 (-> ph (-> ps (-. ch)))) (-> ph (-. ps))
1 dnrd 2 mtod)
(-> ph (-. ps))
edit