pm2.18 Show Code edit
# a.k.a. npipip
## Proof by contradiction
##
## Also called the Law of Clavius.
## Metamath seems to have a fairly short but tricky proof of pm2.18 that
## doesn't detour through dn, nimp, con1, et. al.; but we need those
## anyway and pm2.18 is proven more straightforwardly once we have nimp.
##
thm (pm2.18 () () (-> (-> (-. ph) ph) ph)
(-. ph) ph nimp pm2.43i a3i)
(-> (-> (-. ph) ph) ph)
edit