Theorem bibin2 ≪ | index | src | ≫

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

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

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

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

Axiom use