pm2.01 Show Code edit
## Reductio ad absurdum
thm (pm2.01 () () (-> (-> ph (-. ph)) (-. ph))
ph id
(-> ph ph)
ph id
(-> ph ph)
jc con2i)
(-> (-> ph (-. ph)) (-. ph))
edit