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