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