imim12i Show Code edit
## Inference joining two implications (Bridge)
thm (imim12i () (1 (-> ph ps) 2 (-> ch th)) (-> (-> ps ch) (-> ph th))
2 ps imim2i 1 th imim1i syl)
(-> (-> ps ch) (-> ph th))
edit