Description: It is often convenient to have the antecedent under focus in first position, so we can apply immediate theorem forms (as opposed to deduction, tautology form). This series of theorems swaps the first with the last antecedent in an implication chain. This kind of swapping is self-inverse, whence we prefer it over, say, rotating theorems. A consequent can hide a tail of a longer chain, so theorems of this series appear as swapping a pair of antecedents with fixed offsets. This form of swapping antecedents is flexible enough to allow for any permutation of antecedents in an implication chain.
The first elements of this series correspond to com12 , com13 , com14 and com15 in the main part.
The proofs of this series aim at automated proving using a simple recursive scheme. It employs the previous theorem in the series along with a sample from the wl-impchain-mp-x series developed before. (Contributed by Wolf Lammen, 17-Nov-2019)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-impchain-com-1.x |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tru |