pm2.18i Show Code edit
## Proof by contradiction
thm (pm2.18i () (1 (-> (-. ph) ph)) ph
1 ph pm2.18 ax-mp)
ph
edit