theorem anw4l (a b c d e f: wff): $ a -> f $ > $ a /\ b /\ c /\ d /\ e -> f $;
a -> f
a /\ b -> f
a /\ b /\ c /\ d /\ e -> f