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