theorem imim2d (a b c d: wff): $ a -> c -> d $ > $ a -> (b -> c) -> b -> d $;
(c -> d) -> (b -> c) -> b -> d
a -> c -> d
a -> (b -> c) -> b -> d