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