Theorem con3bb ≪ | index | src | ≫

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

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

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

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

Axiom use