Theorem orim1 ≪ | index | src | ≫

theorem orim1 (a b c: wff): $ (a -> b) -> a \/ c -> b \/ c $;

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

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

Axiom use