Description: Lemma 2 for upgr1wlkd . (Contributed by AV, 22-Jan-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | upgr1wlkd.p | |
|
upgr1wlkd.f | |
||
upgr1wlkd.x | |
||
upgr1wlkd.y | |
||
upgr1wlkd.j | |
||
Assertion | upgr1wlkdlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | upgr1wlkd.p | |
|
2 | upgr1wlkd.f | |
|
3 | upgr1wlkd.x | |
|
4 | upgr1wlkd.y | |
|
5 | upgr1wlkd.j | |
|
6 | ssid | |
|
7 | sseq2 | |
|
8 | 7 | adantl | |
9 | 6 8 | mpbiri | |
10 | 5 9 | mpidan | |