Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-impchain-mp-x | Structured version Visualization version GIF version |
Description: This series of theorems provide a means of exchanging the consequent of an implication chain via a simple implication. In the main part, the theorems ax-mp 5, syl 17, syl6 34, syl8 73 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 |
---|---|
wl-impchain-mp-x | ⊢ ⊤ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1478 | 1 ⊢ ⊤ |
Colors of variables: wff setvar class |
Syntax hints: ⊤wtru 1475 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 195 df-tru 1477 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |