condan Show Code edit
## Proof by contradiction
thm (condan () (condan.1 (-> (/\ ph (-. ps)) ch) condan.2 (-> (/\ ph (-. ps)) (-. ch))) (-> ph ps) condan.1 ex condan.2 ex pm2.65d ps notnot2 syl)
(-> ph ps)
edit