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