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