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