Proof of Theorem swrdccat3a
Step | Hyp | Ref
| Expression |
1 | | elfznn0 12433 |
. . . . . 6
|
2 | | 0elfz 12436 |
. . . . . 6
|
3 | 1, 2 | syl 17 |
. . . . 5
|
4 | 3 | ancri 575 |
. . . 4
|
5 | | swrdccatin12.l |
. . . . . 6
|
6 | 5 | swrdccat3 13492 |
. . . . 5
Word
Word
++ substr substr
substr substr ++ substr |
7 | 6 | imp 445 |
. . . 4
Word
Word
++ substr substr
substr substr ++ substr |
8 | 4, 7 | sylan2 491 |
. . 3
Word
Word ++ substr substr
substr substr ++ substr |
9 | | iftrue 4092 |
. . . . 5
substr
++ substr substr |
10 | 9 | adantl 482 |
. . . 4
Word Word
substr ++ substr substr |
11 | | iffalse 4095 |
. . . . . 6
substr ++ substr ++ substr |
12 | 11 | 3ad2ant2 1083 |
. . . . 5
Word Word
substr ++ substr ++ substr |
13 | | lencl 13324 |
. . . . . . . . . . . . 13
Word |
14 | 5, 13 | syl5eqel 2705 |
. . . . . . . . . . . 12
Word |
15 | | nn0le0eq0 11321 |
. . . . . . . . . . . 12
|
16 | 14, 15 | syl 17 |
. . . . . . . . . . 11
Word
|
17 | 16 | biimpd 219 |
. . . . . . . . . 10
Word |
18 | 17 | adantr 481 |
. . . . . . . . 9
Word
Word |
19 | 5 | eqeq1i 2627 |
. . . . . . . . . . . . . . . 16
|
20 | 19 | biimpi 206 |
. . . . . . . . . . . . . . 15
|
21 | | hasheq0 13154 |
. . . . . . . . . . . . . . 15
Word
|
22 | 20, 21 | syl5ib 234 |
. . . . . . . . . . . . . 14
Word
|
23 | 22 | adantr 481 |
. . . . . . . . . . . . 13
Word
Word |
24 | 23 | imp 445 |
. . . . . . . . . . . 12
Word
Word
|
25 | | 0m0e0 11130 |
. . . . . . . . . . . . . . . 16
|
26 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
27 | 26 | eqcoms 2630 |
. . . . . . . . . . . . . . . 16
|
28 | 25, 27 | syl5eqr 2670 |
. . . . . . . . . . . . . . 15
|
29 | 28 | adantl 482 |
. . . . . . . . . . . . . 14
Word
Word
|
30 | 29 | opeq1d 4408 |
. . . . . . . . . . . . 13
Word
Word
|
31 | 30 | oveq2d 6666 |
. . . . . . . . . . . 12
Word
Word
substr substr |
32 | 24, 31 | oveq12d 6668 |
. . . . . . . . . . 11
Word
Word
++
substr
++ substr |
33 | | swrdcl 13419 |
. . . . . . . . . . . . . 14
Word substr
Word |
34 | | ccatlid 13369 |
. . . . . . . . . . . . . 14
substr
Word ++ substr substr |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . 13
Word ++ substr
substr |
36 | 35 | adantl 482 |
. . . . . . . . . . . 12
Word
Word
++ substr substr |
37 | 36 | adantr 481 |
. . . . . . . . . . 11
Word
Word
++ substr substr |
38 | 32, 37 | eqtrd 2656 |
. . . . . . . . . 10
Word
Word
++
substr substr |
39 | 38 | ex 450 |
. . . . . . . . 9
Word
Word ++ substr substr |
40 | 18, 39 | syld 47 |
. . . . . . . 8
Word
Word ++ substr substr |
41 | 40 | adantr 481 |
. . . . . . 7
Word
Word
++
substr substr |
42 | 41 | imp 445 |
. . . . . 6
Word Word
++
substr substr |
43 | 42 | 3adant2 1080 |
. . . . 5
Word Word
++
substr substr |
44 | 12, 43 | eqtrd 2656 |
. . . 4
Word Word
substr ++ substr substr |
45 | 11 | 3ad2ant2 1083 |
. . . . 5
Word Word
substr
++ substr ++ substr |
46 | 5 | opeq2i 4406 |
. . . . . . . . . . 11
|
47 | 46 | oveq2i 6661 |
. . . . . . . . . 10
substr substr |
48 | | swrdid 13428 |
. . . . . . . . . 10
Word substr |
49 | 47, 48 | syl5req 2669 |
. . . . . . . . 9
Word substr |
50 | 49 | adantr 481 |
. . . . . . . 8
Word
Word substr |
51 | 50 | adantr 481 |
. . . . . . 7
Word
Word substr |
52 | 51 | 3ad2ant1 1082 |
. . . . . 6
Word Word
substr |
53 | 52 | oveq1d 6665 |
. . . . 5
Word Word
++ substr substr ++ substr |
54 | 45, 53 | eqtrd 2656 |
. . . 4
Word Word
substr
++ substr substr ++ substr |
55 | 10, 44, 54 | 2if2 4136 |
. . 3
Word
Word substr ++ substr substr
substr substr ++ substr |
56 | 8, 55 | eqtr4d 2659 |
. 2
Word
Word ++ substr substr ++ substr |
57 | 56 | ex 450 |
1
Word
Word ++ substr
substr
++ substr |