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