pm2.24 Show Code edit
## Contradiction Implies Anything
thm (pm2.24 () () (-> ph (-> (-. ph) ps))
ph ps pm2.21 com12)
(-> ph (-> (-. ph) ps))
edit