Theorem bibi1 ≪ | index | src | ≫

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

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

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

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

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

Axiom use