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