|Description: This series of theorems
allow swapping any two antecedents in an
implication chain. The theorem names follow a pattern wl-impchain-com-n.m
with integral numbers n < m, that swaps the m-th antecedent with n-th
in an implication chain. It is sufficient to restrict the length of the
chain to m, too, since the consequent can be assumed to be the tail right
of the m-th antecedent of any arbitrary sized implication chain. We
further assume n > 1, since the wl-impchain-com-1.x 33586 series already
covers the special case n = 1.
Being able to swap any two antecedents in an implication chain lays the
foundation of permuting its antecedents arbitrarily.
The proofs of this series aim at automated proofing using a simple scheme.
Any instance of this series is a triple step of swapping the first and
n-th antecedent, then the first and the m-th, then the first and the n-th
antecedent again. Each of these steps is an instance of the
wl-impchain-com-1.x 33586 series. (Contributed by Wolf