theorem mtand (a b c: wff): $ a -> ~b $ > $ a /\ c -> b $ > $ a -> ~c $;
a -> ~b
a /\ c -> b
a -> c -> b
a -> ~c