Step | Hyp | Ref
| Expression |
1 | | uhgr3cyclex.e |
. . . . . . 7
Edg |
2 | 1 | eleq2i 2693 |
. . . . . 6
Edg |
3 | | eqid 2622 |
. . . . . . 7
iEdg iEdg |
4 | 3 | uhgredgiedgb 26021 |
. . . . . 6
UHGraph Edg
iEdg
iEdg |
5 | 2, 4 | syl5bb 272 |
. . . . 5
UHGraph iEdg iEdg |
6 | 1 | eleq2i 2693 |
. . . . . 6
Edg |
7 | 3 | uhgredgiedgb 26021 |
. . . . . 6
UHGraph Edg
iEdg
iEdg |
8 | 6, 7 | syl5bb 272 |
. . . . 5
UHGraph iEdg iEdg |
9 | 1 | eleq2i 2693 |
. . . . . 6
Edg |
10 | 3 | uhgredgiedgb 26021 |
. . . . . 6
UHGraph Edg
iEdg
iEdg |
11 | 9, 10 | syl5bb 272 |
. . . . 5
UHGraph iEdg iEdg |
12 | 5, 8, 11 | 3anbi123d 1399 |
. . . 4
UHGraph
iEdg iEdg
iEdg
iEdg
iEdg iEdg |
13 | 12 | adantr 481 |
. . 3
UHGraph
iEdg iEdg
iEdg iEdg
iEdg iEdg |
14 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
15 | | eqid 2622 |
. . . . . . . . . . . . . 14
|
16 | | 3simpa 1058 |
. . . . . . . . . . . . . . . . 17
|
17 | | pm3.22 465 |
. . . . . . . . . . . . . . . . . 18
|
18 | 17 | 3adant2 1080 |
. . . . . . . . . . . . . . . . 17
|
19 | 16, 18 | jca 554 |
. . . . . . . . . . . . . . . 16
|
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . 15
|
21 | 20 | ad2antlr 763 |
. . . . . . . . . . . . . 14
UHGraph
iEdg
iEdg iEdg
iEdg iEdg
iEdg
|
22 | | 3simpa 1058 |
. . . . . . . . . . . . . . . . 17
|
23 | | necom 2847 |
. . . . . . . . . . . . . . . . . . . . 21
|
24 | 23 | biimpi 206 |
. . . . . . . . . . . . . . . . . . . 20
|
25 | 24 | anim1i 592 |
. . . . . . . . . . . . . . . . . . 19
|
26 | 25 | ancomd 467 |
. . . . . . . . . . . . . . . . . 18
|
27 | 26 | 3adant2 1080 |
. . . . . . . . . . . . . . . . 17
|
28 | | necom 2847 |
. . . . . . . . . . . . . . . . . . 19
|
29 | 28 | biimpi 206 |
. . . . . . . . . . . . . . . . . 18
|
30 | 29 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . . 17
|
31 | 22, 27, 30 | 3jca 1242 |
. . . . . . . . . . . . . . . 16
|
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . 15
|
33 | 32 | ad2antlr 763 |
. . . . . . . . . . . . . 14
UHGraph
iEdg
iEdg iEdg
iEdg iEdg
iEdg |
34 | | eqimss 3657 |
. . . . . . . . . . . . . . . . . 18
iEdg
iEdg |
35 | 34 | adantl 482 |
. . . . . . . . . . . . . . . . 17
iEdg
iEdg iEdg |
36 | 35 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . 16
iEdg iEdg iEdg
iEdg iEdg
iEdg iEdg |
37 | | eqimss 3657 |
. . . . . . . . . . . . . . . . . 18
iEdg
iEdg |
38 | 37 | adantl 482 |
. . . . . . . . . . . . . . . . 17
iEdg
iEdg iEdg |
39 | 38 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . 16
iEdg iEdg iEdg
iEdg iEdg
iEdg iEdg |
40 | | eqimss 3657 |
. . . . . . . . . . . . . . . . . 18
iEdg
iEdg |
41 | 40 | adantl 482 |
. . . . . . . . . . . . . . . . 17
iEdg
iEdg iEdg |
42 | 41 | 3ad2ant2 1083 |
. . . . . . . . . . . . . . . 16
iEdg iEdg iEdg
iEdg iEdg
iEdg iEdg |
43 | 36, 39, 42 | 3jca 1242 |
. . . . . . . . . . . . . . 15
iEdg iEdg iEdg
iEdg iEdg
iEdg
iEdg
iEdg
iEdg |
44 | 43 | adantl 482 |
. . . . . . . . . . . . . 14
UHGraph
iEdg
iEdg iEdg
iEdg iEdg
iEdg iEdg
iEdg iEdg |
45 | | uhgr3cyclex.v |
. . . . . . . . . . . . . 14
Vtx |
46 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . 19
|
47 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 46, 47 | jca 554 |
. . . . . . . . . . . . . . . . . 18
|
49 | 48, 30 | anim12i 590 |
. . . . . . . . . . . . . . . . 17
|
50 | 49 | adantl 482 |
. . . . . . . . . . . . . . . 16
UHGraph
|
51 | | pm3.22 465 |
. . . . . . . . . . . . . . . . 17
iEdg iEdg iEdg
iEdg iEdg
iEdg iEdg
iEdg |
52 | 51 | 3adant2 1080 |
. . . . . . . . . . . . . . . 16
iEdg iEdg iEdg
iEdg iEdg
iEdg iEdg
iEdg iEdg
iEdg |
53 | 45, 1, 3 | uhgr3cyclexlem 27041 |
. . . . . . . . . . . . . . . 16
iEdg iEdg iEdg
iEdg |
54 | 50, 52, 53 | syl2an 494 |
. . . . . . . . . . . . . . 15
UHGraph
iEdg
iEdg iEdg
iEdg iEdg
iEdg |
55 | | 3simpc 1060 |
. . . . . . . . . . . . . . . . . 18
|
56 | | simp3 1063 |
. . . . . . . . . . . . . . . . . 18
|
57 | 55, 56 | anim12i 590 |
. . . . . . . . . . . . . . . . 17
|
58 | 57 | adantl 482 |
. . . . . . . . . . . . . . . 16
UHGraph
|
59 | | 3simpc 1060 |
. . . . . . . . . . . . . . . 16
iEdg iEdg iEdg
iEdg iEdg
iEdg iEdg
iEdg iEdg
iEdg |
60 | 45, 1, 3 | uhgr3cyclexlem 27041 |
. . . . . . . . . . . . . . . . 17
iEdg iEdg iEdg
iEdg |
61 | 60 | necomd 2849 |
. . . . . . . . . . . . . . . 16
iEdg iEdg iEdg
iEdg |
62 | 58, 59, 61 | syl2an 494 |
. . . . . . . . . . . . . . 15
UHGraph
iEdg
iEdg iEdg
iEdg iEdg
iEdg |
63 | 45, 1, 3 | uhgr3cyclexlem 27041 |
. . . . . . . . . . . . . . . . . . . . . . . 24
iEdg iEdg iEdg
iEdg |
64 | 63 | exp31 630 |
. . . . . . . . . . . . . . . . . . . . . . 23
iEdg
iEdg iEdg
iEdg |
65 | 64 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . 22
iEdg
iEdg iEdg
iEdg |
66 | 65 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
iEdg iEdg iEdg
iEdg |
67 | 66 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . . . . . . 20
iEdg iEdg iEdg
iEdg |
68 | 67 | impcom 446 |
. . . . . . . . . . . . . . . . . . 19
iEdg
iEdg iEdg
iEdg |
69 | 68 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
UHGraph
iEdg
iEdg iEdg
iEdg |
70 | 69 | com12 32 |
. . . . . . . . . . . . . . . . 17
iEdg iEdg iEdg
iEdg UHGraph |
71 | 70 | 3adant3 1081 |
. . . . . . . . . . . . . . . 16
iEdg iEdg iEdg
iEdg iEdg
iEdg UHGraph |
72 | 71 | impcom 446 |
. . . . . . . . . . . . . . 15
UHGraph
iEdg
iEdg iEdg
iEdg iEdg
iEdg |
73 | 54, 62, 72 | 3jca 1242 |
. . . . . . . . . . . . . 14
UHGraph
iEdg
iEdg iEdg
iEdg iEdg
iEdg |
74 | | eqidd 2623 |
. . . . . . . . . . . . . 14
UHGraph
iEdg
iEdg iEdg
iEdg iEdg
iEdg |
75 | 14, 15, 21, 33, 44, 45, 3, 73, 74 | 3cyclpd 27039 |
. . . . . . . . . . . . 13
UHGraph
iEdg
iEdg iEdg
iEdg iEdg
iEdg Cycles |
76 | | s3cli 13626 |
. . . . . . . . . . . . . . 15
Word |
77 | 76 | elexi 3213 |
. . . . . . . . . . . . . 14
|
78 | | s4cli 13627 |
. . . . . . . . . . . . . . 15
Word |
79 | 78 | elexi 3213 |
. . . . . . . . . . . . . 14
|
80 | | breq12 4658 |
. . . . . . . . . . . . . . 15
Cycles
Cycles |
81 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
|
82 | 81 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
|
83 | 82 | adantr 481 |
. . . . . . . . . . . . . . 15
|
84 | | fveq1 6190 |
. . . . . . . . . . . . . . . . 17
|
85 | 84 | eqeq1d 2624 |
. . . . . . . . . . . . . . . 16
|
86 | 85 | adantl 482 |
. . . . . . . . . . . . . . 15
|
87 | 80, 83, 86 | 3anbi123d 1399 |
. . . . . . . . . . . . . 14
Cycles
Cycles |
88 | 77, 79, 87 | spc2ev 3301 |
. . . . . . . . . . . . 13
Cycles
Cycles |
89 | 75, 88 | syl 17 |
. . . . . . . . . . . 12
UHGraph
iEdg
iEdg iEdg
iEdg iEdg
iEdg Cycles |
90 | 89 | expcom 451 |
. . . . . . . . . . 11
iEdg iEdg iEdg
iEdg iEdg
iEdg UHGraph Cycles |
91 | 90 | 3exp 1264 |
. . . . . . . . . 10
iEdg
iEdg iEdg iEdg iEdg iEdg UHGraph
Cycles |
92 | 91 | rexlimiva 3028 |
. . . . . . . . 9
iEdg iEdg iEdg iEdg iEdg iEdg UHGraph
Cycles |
93 | 92 | com12 32 |
. . . . . . . 8
iEdg
iEdg
iEdg iEdg
iEdg
iEdg UHGraph
Cycles |
94 | 93 | rexlimiva 3028 |
. . . . . . 7
iEdg iEdg
iEdg iEdg
iEdg
iEdg UHGraph
Cycles |
95 | 94 | com13 88 |
. . . . . 6
iEdg
iEdg
iEdg iEdg
iEdg iEdg UHGraph
Cycles |
96 | 95 | rexlimiva 3028 |
. . . . 5
iEdg iEdg
iEdg iEdg
iEdg iEdg UHGraph
Cycles |
97 | 96 | 3imp 1256 |
. . . 4
iEdg iEdg
iEdg
iEdg
iEdg iEdg UHGraph Cycles |
98 | 97 | com12 32 |
. . 3
UHGraph
iEdg
iEdg
iEdg iEdg
iEdg iEdg Cycles |
99 | 13, 98 | sylbid 230 |
. 2
UHGraph
Cycles |
100 | 99 | 3impia 1261 |
1
UHGraph
Cycles |