a1i Show Code edit
## First Axiom Inference
##
## [ ph
## (-> ps [ ph)
##
thm (a1i () (1 ph) (-> ps ph)
1 ph ps ax-1 ax-mp)
(-> ps ph)
edit