Theorem bian1a ≪ | index | src | ≫

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

a /\ b <-> b /\ a

(b -> a) -> (b /\ a <-> b)

(b -> a) -> (a /\ b <-> b)

Axiom use