Description: Lemma 2 for wlkiswwlks2 . (Contributed by Alexander van der Vekens, 20-Jul-2018)
Ref | Expression | ||
---|---|---|---|
Hypothesis | wlkiswwlks2lem.f | |
|
Assertion | wlkiswwlks2lem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wlkiswwlks2lem.f | |
|
2 | fveq2 | |
|
3 | fvoveq1 | |
|
4 | 2 3 | preq12d | |
5 | 4 | fveq2d | |
6 | simpr | |
|
7 | fvexd | |
|
8 | 1 5 6 7 | fvmptd3 | |