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