Theorem con1bb ≪ | index | src | ≫

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

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

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

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

Axiom use