Theorem biim1 ≪ | index | src | ≫

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

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

a -> ~a -> b

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

Axiom use