pm2.24i Show Code edit
## Contradiction Implies Anything
##
## The theorem pm2.24 written as an inference.
##
thm (pm2.24i () (1 ph) (-> (-. ph) ps)
1 ph ps pm2.24 ax-mp)
(-> (-. ph) ps)
edit