pm2.21 Show Code edit
# a.k.a. a1n
## Contradiction Implies Anything
##
## From a wff and its negation, anything is true. Also called the
## Duns Scotus law.
##
thm (pm2.21 () () (-> (-. ph) (-> ph ps))
ps ph ax-3 himp1i)
(-> (-. ph) (-> ph ps))
edit