ecase3d Show Code edit
## Elimination by cases
thm (ecase3d () (ecase3d.1 (-> ph (-> ps th)) ecase3d.2 (-> ph (-> ch th)) ecase3d.3 (-> ph (-> (-. (\/ ps ch)) th))) (-> ph th) ecase3d.1 com12 ecase3d.2 com12 ecase3d.3 com12 ecase3)
(-> ph th)
edit