a2i Show Code edit
## Second Axiom Inference
##
## (-> ph ] (-> [ ps ] [ ch))
## (-> (-> ph ] [ ps ] ) (-> ph [ ch))
##
thm (a2i () (1 (-> ph (-> ps ch))) (-> (-> ph ps) (-> ph ch))
1 ph ps ch ax-2 ax-mp)
(-> (-> ph ps) (-> ph ch))
edit