Metamath Proof Explorer
Description: Lemma 2 for 3wlkd . (Contributed by AV, 7-Feb-2021)
|
|
Ref |
Expression |
|
Hypotheses |
3wlkd.p |
|
|
|
3wlkd.f |
|
|
Assertion |
3wlkdlem2 |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
3wlkd.p |
|
2 |
|
3wlkd.f |
|
3 |
2
|
fveq2i |
|
4 |
|
s3len |
|
5 |
3 4
|
eqtri |
|
6 |
5
|
oveq2i |
|
7 |
|
fzo0to3tp |
|
8 |
6 7
|
eqtri |
|