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