imim12d Show Code edit
## Deduction combining antecedents and consequents
thm (imim12d () (1 (-> ph (-> ps ch)) 2 (-> ph (-> th ta)))
(-> ph (-> (-> ch th) (-> ps ta)))
2 ch imim2d 1 ta imim1d syld)
(-> ph (-> (-> ch th) (-> ps ta)))
edit