mt2i Show Code edit
## Modus Tollens
thm (mt2i () (1 ch 2 (-> ph (-> ps (-. ch)))) (-> ph (-. ps))
1 dnri 2 mtoi)
(-> ph (-. ps))
edit