Theorem bieq2 ≪ | index | src | ≫

theorem bieq2 (a b c: wff): $ (b <-> c) -> (a <-> b <-> (a <-> c)) $;

(b <-> c) -> (b <-> c)

(b <-> c) -> (a <-> b <-> (a <-> c))

Axiom use