Theorem bieq1 ≪ | index | src | ≫

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

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

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

Axiom use