Description: This theorem is in fact a copy of com3r . The proof is an example of
how to arrive at arbitrary permutations of antecedents, using only
swapping theorems. The recursion principle is to first swap the correct
antecedent to the position just before the consequent, and then employ a
theorem handling an implication chain of length one less to reorder the
others. (Contributed by Wolf Lammen, 17-Nov-2019)(Proof modification is discouraged.)(New usage is discouraged.)