Metamath Proof Explorer


Theorem wl-impchain-mp-x

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)

Ref Expression
Assertion wl-impchain-mp-x
|- T.

Proof

Step Hyp Ref Expression
1 tru
 |-  T.