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