Theorem wl-impchain-com-n.m

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 one 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 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 series. (Contributed by Wolf Lammen, 17-Nov-2019)

	Ref	Expression
Assertion	wl-impchain-com-n.m	|- T.

Proof

Step	Hyp	Ref	Expression
1		tru	|- T.