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