Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > wl-impchain-mp-0 | Structured version Visualization version GIF version |
Description: This theorem is the start
of a proof recursion scheme where we replace
the consequent of an implication chain. The number '0' in the theorem
name indicates that the modified chain has no antecedents.
This theorem is in fact a copy of ax-mp 5, and is repeated here to emphasize the recursion using similar theorem names. (Contributed by Wolf Lammen, 6-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
wl-impchain-mp-0.a | ⊢ 𝜓 |
wl-impchain-mp-0.b | ⊢ (𝜓 → 𝜑) |
Ref | Expression |
---|---|
wl-impchain-mp-0 | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wl-impchain-mp-0.a | . 2 ⊢ 𝜓 | |
2 | wl-impchain-mp-0.b | . 2 ⊢ (𝜓 → 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 |
This theorem is referenced by: wl-impchain-mp-1 33610 wl-impchain-com-1.2 33614 |
Copyright terms: Public domain | W3C validator |