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