ecase2d Show Code edit
## Elimination by cases
thm (ecase2d () (ecase2d.1 (-> ph ps) ecase2d.2 (-> ph (-. (/\ ps ch))) ecase2d.3 (-> ph (-. (/\ ps th))) ecase2d.4 (-> ph (\/ ta (\/ ch th)))) (-> ph ta) ecase2d.1 ecase2d.2 ps ch imnan sylibr mpd ecase2d.1 ecase2d.3 ps th imnan sylibr mpd jca ch th ioran sylibr ecase2d.4 ta (\/ ch th) orcom sylib ord mpd)
(-> ph ta)
edit