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