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