pm2.65 Show Code edit
## Proof by contradiction
thm (pm2.65 () () (-> (-> ph ps) (-> (-> ph (-. ps)) (-. ph)))
ph ps (-. ph) imim1 ph ps con2 syl5 ph pm2.01 syl6)
(-> (-> ph ps) (-> (-> ph (-. ps)) (-. ph)))
edit