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