a3i Show Code edit
# Yeah, negation!
## Third Axiom Inference
thm (a3i () (1 (-> (-. ph) (-. ps))) (-> ps ph)
1 ph ps ax-3 ax-mp)
(-> ps ph)
edit