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