jc Show Code edit
## Join the consequents of two premises
thm (jc () (1 (-> ph ps) 2 (-> ph ch)) (-> ph (-. (-> ps (-. ch))))
2 1 ps ch preand syl mpd)
(-> ph (-. (-> ps (-. ch))))
edit