imim2d Show Code edit
## Deduction adding nested antecedents
thm (imim2d () (1 (-> ph (-> ps ch))) (-> ph (-> (-> th ps) (-> th ch)))
1 th a1i com12 a2d)
(-> ph (-> (-> th ps) (-> th ch)))
edit