Theorem biim2 ≪ | index | src | ≫

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

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

~b -> b -> ~a

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

Axiom use