ecase3 Show Code edit
## Elimination by cases
thm (ecase3 () (ecase3.1 (-> ph ch) ecase3.2 (-> ps ch) ecase3.3 (-> (-. (\/ ph ps)) ch)) ch ph ps ioran ecase3.3 sylbir ex ecase3.1 ecase3.2 pm2.61ii)
ch
edit