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