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