pm2.18_mm Show Code edit
## Proof by contradiction
thm (pm2.18_mm () () (-> (-> (-. ph) ph) ph)
ph (-. (-> (-. ph) ph)) pm2.21 a2i a3d pm2.43i)
(-> (-> (-. ph) ph) ph)
edit