Theorem bian1 ≪ | index | src | ≫

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

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

a -> b -> a

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

Axiom use