pm2.01d Show Code edit
## Reductio ad absurdum
##
## The theorem pm2.01 written as an deduction.
##
thm (pm2.01d () (1 (-> ph (-> ps (-. ps)))) (-> ph (-. ps))
1 ps pm2.01 syl)
(-> ph (-. ps))
edit