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