theorem bi2a (a b c: wff): $ a -> (b <-> c) $ > $ a /\ c -> b $;
a -> (b <-> c)
a -> c -> b
a /\ c -> b