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