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