Theorem con2bb ≪ | index | src | ≫

theorem con2bb (a b: wff): $ a <-> ~b <-> (b <-> ~a) $;

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

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

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

Axiom use