Description: This series of theorems provide a means of exchanging the consequent of an
implication chain via a simple implication. In the main part, Theorems
ax-mp , syl , syl6 , syl8 form the beginning of this series.
These theorems are replicated here, but with proofs that aim at a
recursive scheme, allowing to base a proof on that of the previous one in
the series. (Contributed by Wolf Lammen, 17-Nov-2019)