ecase23d Show Code edit
# Deduction for elimination by cases.
thm (ecase23d () (ecase23d.1 (-> ph (-. ch)) ecase23d.2 (-> ph (-. th)) ecase23d.3 (-> ph (\/\/ ps ch th))) (-> ph ps) ecase23d.1 ecase23d.2 jca ch th ioran sylibr ecase23d.3 ps ch th 3orass sylib ord mt3d)
(-> ph ps)
edit