mt3d Show Code edit
## Modus Tollens
thm (mt3d () (1 (-> ph (-. ch)) 2 (-> ph (-> (-. ps) ch))) (-> ph ps)
1 2 con1d mpd)
(-> ph ps)
edit