Description: Lemma 2 for clwlkclwwlkf1 . (Contributed by AV, 24-May-2022) (Revised by AV, 30-Oct-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | clwlkclwwlkf.c | |
|
clwlkclwwlkf.a | |
||
clwlkclwwlkf.b | |
||
clwlkclwwlkf.d | |
||
clwlkclwwlkf.e | |
||
Assertion | clwlkclwwlkf1lem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clwlkclwwlkf.c | |
|
2 | clwlkclwwlkf.a | |
|
3 | clwlkclwwlkf.b | |
|
4 | clwlkclwwlkf.d | |
|
5 | clwlkclwwlkf.e | |
|
6 | 1 2 3 | clwlkclwwlkflem | |
7 | 1 4 5 | clwlkclwwlkflem | |
8 | 6 7 | anim12i | |
9 | eqid | |
|
10 | 9 | wlkpwrd | |
11 | 10 | 3ad2ant1 | |
12 | 9 | wlkpwrd | |
13 | 12 | 3ad2ant1 | |
14 | 11 13 | anim12i | |
15 | nnnn0 | |
|
16 | 15 | 3ad2ant3 | |
17 | nnnn0 | |
|
18 | 17 | 3ad2ant3 | |
19 | 16 18 | anim12i | |
20 | wlklenvp1 | |
|
21 | nnre | |
|
22 | 21 | lep1d | |
23 | breq2 | |
|
24 | 22 23 | syl5ibr | |
25 | 20 24 | syl | |
26 | 25 | a1d | |
27 | 26 | 3imp | |
28 | wlklenvp1 | |
|
29 | nnre | |
|
30 | 29 | lep1d | |
31 | breq2 | |
|
32 | 30 31 | syl5ibr | |
33 | 28 32 | syl | |
34 | 33 | a1d | |
35 | 34 | 3imp | |
36 | 27 35 | anim12i | |
37 | 14 19 36 | 3jca | |
38 | pfxeq | |
|
39 | 8 37 38 | 3syl | |
40 | 39 | biimp3a | |