Description: A prefix of a concatenation being a prefix of the first concatenated word. (Contributed by AV, 10-May-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | swrdccatin2.l | |
|
Assertion | pfxccatpfx1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | swrdccatin2.l | |
|
2 | 3simpa | |
|
3 | elfznn0 | |
|
4 | 0elfz | |
|
5 | 3 4 | syl | |
6 | 1 | oveq2i | |
7 | 6 | eleq2i | |
8 | 7 | biimpi | |
9 | 5 8 | jca | |
10 | 9 | 3ad2ant3 | |
11 | swrdccatin1 | |
|
12 | 2 10 11 | sylc | |
13 | ccatcl | |
|
14 | 13 | 3adant3 | |
15 | 3 | 3ad2ant3 | |
16 | 14 15 | jca | |
17 | pfxval | |
|
18 | 16 17 | syl | |
19 | pfxval | |
|
20 | 3 19 | sylan2 | |
21 | 20 | 3adant2 | |
22 | 12 18 21 | 3eqtr4d | |