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