a2d Show Code edit
## Second Axiom Deduction
##
## (-> ph (-> ps ] (-> [ ch ] [ th)))
## (-> ph (-> (-> ps ] [ ch ] ) (-> ps [ th)))
##
thm (a2d () (1 (-> ph (-> ps (-> ch th)))) (-> ph (-> (-> ps ch) (-> ps th)))
1 ps ch th ax-2 syl)
(-> ph (-> (-> ps ch) (-> ps th)))
edit