Theorem bior1 ≪ | index | src | ≫

theorem bior1 (a b: wff): $ ~a -> (a \/ b <-> b) $;

(a -> b) -> (a \/ b <-> b)

~a -> a -> b

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

Axiom use