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