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