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