theorem con3 (a b: wff): $ (a -> b) -> ~b -> ~a $;
(a -> ~~b) -> ~b -> ~a
b -> ~~b
(a -> b) -> a -> ~~b
(a -> b) -> ~b -> ~a