Step | Hyp | Ref
| Expression |
1 | | frgr3v.v |
. . . . . 6
Vtx |
2 | | frgr3v.e |
. . . . . 6
Edg |
3 | 1, 2 | frgrusgrfrcond 27123 |
. . . . 5
FriendGraph USGraph
|
4 | 3 | a1i 11 |
. . . 4
USGraph
FriendGraph USGraph
|
5 | | id 22 |
. . . . . . . 8
|
6 | | difeq1 3721 |
. . . . . . . . 9
|
7 | | reueq1 3140 |
. . . . . . . . 9
|
8 | 6, 7 | raleqbidv 3152 |
. . . . . . . 8
|
9 | 5, 8 | raleqbidv 3152 |
. . . . . . 7
|
10 | 9 | anbi2d 740 |
. . . . . 6
USGraph
USGraph
|
11 | 10 | baibd 948 |
. . . . 5
USGraph USGraph
|
12 | 11 | adantl 482 |
. . . 4
USGraph USGraph
|
13 | 4, 12 | bitrd 268 |
. . 3
USGraph
FriendGraph
|
14 | | sneq 4187 |
. . . . . . . 8
|
15 | 14 | difeq2d 3728 |
. . . . . . 7
|
16 | | preq2 4269 |
. . . . . . . . . 10
|
17 | 16 | preq1d 4274 |
. . . . . . . . 9
|
18 | 17 | sseq1d 3632 |
. . . . . . . 8
|
19 | 18 | reubidv 3126 |
. . . . . . 7
|
20 | 15, 19 | raleqbidv 3152 |
. . . . . 6
|
21 | | sneq 4187 |
. . . . . . . 8
|
22 | 21 | difeq2d 3728 |
. . . . . . 7
|
23 | | preq2 4269 |
. . . . . . . . . 10
|
24 | 23 | preq1d 4274 |
. . . . . . . . 9
|
25 | 24 | sseq1d 3632 |
. . . . . . . 8
|
26 | 25 | reubidv 3126 |
. . . . . . 7
|
27 | 22, 26 | raleqbidv 3152 |
. . . . . 6
|
28 | | sneq 4187 |
. . . . . . . 8
|
29 | 28 | difeq2d 3728 |
. . . . . . 7
|
30 | | preq2 4269 |
. . . . . . . . . 10
|
31 | 30 | preq1d 4274 |
. . . . . . . . 9
|
32 | 31 | sseq1d 3632 |
. . . . . . . 8
|
33 | 32 | reubidv 3126 |
. . . . . . 7
|
34 | 29, 33 | raleqbidv 3152 |
. . . . . 6
|
35 | 20, 27, 34 | raltpg 4236 |
. . . . 5
|
36 | 35 | ad2antrr 762 |
. . . 4
USGraph
|
37 | | tprot 4284 |
. . . . . . . . . 10
|
38 | 37 | a1i 11 |
. . . . . . . . 9
|
39 | 38 | difeq1d 3727 |
. . . . . . . 8
|
40 | | necom 2847 |
. . . . . . . . . . . 12
|
41 | 40 | biimpi 206 |
. . . . . . . . . . 11
|
42 | | necom 2847 |
. . . . . . . . . . . 12
|
43 | 42 | biimpi 206 |
. . . . . . . . . . 11
|
44 | 41, 43 | anim12i 590 |
. . . . . . . . . 10
|
45 | 44 | 3adant3 1081 |
. . . . . . . . 9
|
46 | | diftpsn3 4332 |
. . . . . . . . 9
|
47 | 45, 46 | syl 17 |
. . . . . . . 8
|
48 | 39, 47 | eqtrd 2656 |
. . . . . . 7
|
49 | 48 | raleqdv 3144 |
. . . . . 6
|
50 | | tprot 4284 |
. . . . . . . . . . 11
|
51 | 50 | eqcomi 2631 |
. . . . . . . . . 10
|
52 | 51 | a1i 11 |
. . . . . . . . 9
|
53 | 52 | difeq1d 3727 |
. . . . . . . 8
|
54 | | id 22 |
. . . . . . . . . . 11
|
55 | | necom 2847 |
. . . . . . . . . . . 12
|
56 | 55 | biimpi 206 |
. . . . . . . . . . 11
|
57 | 54, 56 | anim12ci 591 |
. . . . . . . . . 10
|
58 | 57 | 3adant2 1080 |
. . . . . . . . 9
|
59 | | diftpsn3 4332 |
. . . . . . . . 9
|
60 | 58, 59 | syl 17 |
. . . . . . . 8
|
61 | 53, 60 | eqtrd 2656 |
. . . . . . 7
|
62 | 61 | raleqdv 3144 |
. . . . . 6
|
63 | | diftpsn3 4332 |
. . . . . . . 8
|
64 | 63 | 3adant1 1079 |
. . . . . . 7
|
65 | 64 | raleqdv 3144 |
. . . . . 6
|
66 | 49, 62, 65 | 3anbi123d 1399 |
. . . . 5
|
67 | 66 | ad2antlr 763 |
. . . 4
USGraph
|
68 | | preq2 4269 |
. . . . . . . . . . 11
|
69 | 68 | preq2d 4275 |
. . . . . . . . . 10
|
70 | 69 | sseq1d 3632 |
. . . . . . . . 9
|
71 | 70 | reubidv 3126 |
. . . . . . . 8
|
72 | | preq2 4269 |
. . . . . . . . . . 11
|
73 | 72 | preq2d 4275 |
. . . . . . . . . 10
|
74 | 73 | sseq1d 3632 |
. . . . . . . . 9
|
75 | 74 | reubidv 3126 |
. . . . . . . 8
|
76 | 71, 75 | ralprg 4234 |
. . . . . . 7
|
77 | 76 | 3adant1 1079 |
. . . . . 6
|
78 | 72 | preq2d 4275 |
. . . . . . . . . . 11
|
79 | 78 | sseq1d 3632 |
. . . . . . . . . 10
|
80 | 79 | reubidv 3126 |
. . . . . . . . 9
|
81 | | preq2 4269 |
. . . . . . . . . . . 12
|
82 | 81 | preq2d 4275 |
. . . . . . . . . . 11
|
83 | 82 | sseq1d 3632 |
. . . . . . . . . 10
|
84 | 83 | reubidv 3126 |
. . . . . . . . 9
|
85 | 80, 84 | ralprg 4234 |
. . . . . . . 8
|
86 | 85 | ancoms 469 |
. . . . . . 7
|
87 | 86 | 3adant2 1080 |
. . . . . 6
|
88 | 81 | preq2d 4275 |
. . . . . . . . . 10
|
89 | 88 | sseq1d 3632 |
. . . . . . . . 9
|
90 | 89 | reubidv 3126 |
. . . . . . . 8
|
91 | 68 | preq2d 4275 |
. . . . . . . . . 10
|
92 | 91 | sseq1d 3632 |
. . . . . . . . 9
|
93 | 92 | reubidv 3126 |
. . . . . . . 8
|
94 | 90, 93 | ralprg 4234 |
. . . . . . 7
|
95 | 94 | 3adant3 1081 |
. . . . . 6
|
96 | 77, 87, 95 | 3anbi123d 1399 |
. . . . 5
|
97 | 96 | ad2antrr 762 |
. . . 4
USGraph
|
98 | 36, 67, 97 | 3bitrd 294 |
. . 3
USGraph
|
99 | 1, 2 | frgr3vlem2 27138 |
. . . . . . 7
USGraph
|
100 | 99 | imp 445 |
. . . . . 6
USGraph
|
101 | | simpll1 1100 |
. . . . . . . 8
USGraph |
102 | | simpll3 1102 |
. . . . . . . 8
USGraph |
103 | | simpll2 1101 |
. . . . . . . 8
USGraph |
104 | 101, 102,
103 | 3jca 1242 |
. . . . . . 7
USGraph
|
105 | | simplr2 1104 |
. . . . . . . 8
USGraph |
106 | | simplr1 1103 |
. . . . . . . 8
USGraph |
107 | 58 | simpld 475 |
. . . . . . . . 9
|
108 | 107 | ad2antlr 763 |
. . . . . . . 8
USGraph |
109 | 105, 106,
108 | 3jca 1242 |
. . . . . . 7
USGraph |
110 | | tpcomb 4286 |
. . . . . . . . . 10
|
111 | 5, 110 | syl6eq 2672 |
. . . . . . . . 9
|
112 | 111 | anim1i 592 |
. . . . . . . 8
USGraph
USGraph |
113 | 112 | adantl 482 |
. . . . . . 7
USGraph
USGraph |
114 | | reueq1 3140 |
. . . . . . . . 9
|
115 | 110, 114 | mp1i 13 |
. . . . . . . 8
USGraph
|
116 | 1, 2 | frgr3vlem2 27138 |
. . . . . . . . 9
USGraph
|
117 | 116 | imp 445 |
. . . . . . . 8
USGraph
|
118 | 115, 117 | bitrd 268 |
. . . . . . 7
USGraph
|
119 | 104, 109,
113, 118 | syl21anc 1325 |
. . . . . 6
USGraph
|
120 | 100, 119 | anbi12d 747 |
. . . . 5
USGraph
|
121 | 103, 102,
101 | 3jca 1242 |
. . . . . . 7
USGraph
|
122 | | simplr3 1105 |
. . . . . . . 8
USGraph |
123 | 106 | necomd 2849 |
. . . . . . . 8
USGraph |
124 | 105 | necomd 2849 |
. . . . . . . 8
USGraph |
125 | 122, 123,
124 | 3jca 1242 |
. . . . . . 7
USGraph |
126 | 37 | eqeq2i 2634 |
. . . . . . . . . 10
|
127 | 126 | biimpi 206 |
. . . . . . . . 9
|
128 | 127 | anim1i 592 |
. . . . . . . 8
USGraph
USGraph |
129 | 128 | adantl 482 |
. . . . . . 7
USGraph
USGraph |
130 | | reueq1 3140 |
. . . . . . . . 9
|
131 | 37, 130 | mp1i 13 |
. . . . . . . 8
USGraph
|
132 | 1, 2 | frgr3vlem2 27138 |
. . . . . . . . 9
USGraph
|
133 | 132 | imp 445 |
. . . . . . . 8
USGraph
|
134 | 131, 133 | bitrd 268 |
. . . . . . 7
USGraph
|
135 | 121, 125,
129, 134 | syl21anc 1325 |
. . . . . 6
USGraph
|
136 | 103, 101,
102 | 3jca 1242 |
. . . . . . 7
USGraph
|
137 | 123, 122,
105 | 3jca 1242 |
. . . . . . 7
USGraph |
138 | | tpcoma 4285 |
. . . . . . . . . . 11
|
139 | 138 | eqeq2i 2634 |
. . . . . . . . . 10
|
140 | 139 | biimpi 206 |
. . . . . . . . 9
|
141 | 140 | anim1i 592 |
. . . . . . . 8
USGraph
USGraph |
142 | 141 | adantl 482 |
. . . . . . 7
USGraph
USGraph |
143 | | reueq1 3140 |
. . . . . . . . 9
|
144 | 138, 143 | mp1i 13 |
. . . . . . . 8
USGraph
|
145 | 1, 2 | frgr3vlem2 27138 |
. . . . . . . . 9
USGraph
|
146 | 145 | imp 445 |
. . . . . . . 8
USGraph
|
147 | 144, 146 | bitrd 268 |
. . . . . . 7
USGraph
|
148 | 136, 137,
142, 147 | syl21anc 1325 |
. . . . . 6
USGraph
|
149 | 135, 148 | anbi12d 747 |
. . . . 5
USGraph
|
150 | 102, 101,
103 | 3jca 1242 |
. . . . . . 7
USGraph
|
151 | 124, 108,
106 | 3jca 1242 |
. . . . . . 7
USGraph |
152 | 51 | eqeq2i 2634 |
. . . . . . . . . 10
|
153 | 152 | biimpi 206 |
. . . . . . . . 9
|
154 | 153 | anim1i 592 |
. . . . . . . 8
USGraph
USGraph |
155 | 154 | adantl 482 |
. . . . . . 7
USGraph
USGraph |
156 | | reueq1 3140 |
. . . . . . . . 9
|
157 | 51, 156 | mp1i 13 |
. . . . . . . 8
USGraph
|
158 | 1, 2 | frgr3vlem2 27138 |
. . . . . . . . 9
USGraph
|
159 | 158 | imp 445 |
. . . . . . . 8
USGraph
|
160 | 157, 159 | bitrd 268 |
. . . . . . 7
USGraph
|
161 | 150, 151,
155, 160 | syl21anc 1325 |
. . . . . 6
USGraph
|
162 | | 3anrev 1049 |
. . . . . . . . 9
|
163 | 162 | biimpi 206 |
. . . . . . . 8
|
164 | 55, 42, 40 | 3anbi123i 1251 |
. . . . . . . . . 10
|
165 | 164 | biimpi 206 |
. . . . . . . . 9
|
166 | 165 | 3com13 1270 |
. . . . . . . 8
|
167 | 163, 166 | anim12i 590 |
. . . . . . 7
|
168 | | tpcoma 4285 |
. . . . . . . . . . 11
|
169 | 37, 168 | eqtri 2644 |
. . . . . . . . . 10
|
170 | 169 | eqeq2i 2634 |
. . . . . . . . 9
|
171 | 170 | biimpi 206 |
. . . . . . . 8
|
172 | 171 | anim1i 592 |
. . . . . . 7
USGraph
USGraph |
173 | | reueq1 3140 |
. . . . . . . . 9
|
174 | 169, 173 | mp1i 13 |
. . . . . . . 8
USGraph
|
175 | 1, 2 | frgr3vlem2 27138 |
. . . . . . . . 9
USGraph
|
176 | 175 | imp 445 |
. . . . . . . 8
USGraph
|
177 | 174, 176 | bitrd 268 |
. . . . . . 7
USGraph
|
178 | 167, 172,
177 | syl2an 494 |
. . . . . 6
USGraph
|
179 | 161, 178 | anbi12d 747 |
. . . . 5
USGraph
|
180 | 120, 149,
179 | 3anbi123d 1399 |
. . . 4
USGraph
|
181 | | prcom 4267 |
. . . . . . . . . 10
|
182 | 181 | eleq1i 2692 |
. . . . . . . . 9
|
183 | 182 | anbi2i 730 |
. . . . . . . 8
|
184 | 183 | anbi2i 730 |
. . . . . . 7
|
185 | | anandir 872 |
. . . . . . 7
|
186 | 184, 185 | bitr4i 267 |
. . . . . 6
|
187 | | prcom 4267 |
. . . . . . . . . 10
|
188 | 187 | eleq1i 2692 |
. . . . . . . . 9
|
189 | 188 | anbi2i 730 |
. . . . . . . 8
|
190 | 189 | anbi2i 730 |
. . . . . . 7
|
191 | | anandir 872 |
. . . . . . 7
|
192 | 190, 191 | bitr4i 267 |
. . . . . 6
|
193 | | prcom 4267 |
. . . . . . . . . 10
|
194 | 193 | eleq1i 2692 |
. . . . . . . . 9
|
195 | 194 | anbi2i 730 |
. . . . . . . 8
|
196 | 195 | anbi2i 730 |
. . . . . . 7
|
197 | | anandir 872 |
. . . . . . 7
|
198 | 196, 197 | bitr4i 267 |
. . . . . 6
|
199 | 186, 192,
198 | 3anbi123i 1251 |
. . . . 5
|
200 | | 3anrot 1043 |
. . . . . . 7
|
201 | | df-3an 1039 |
. . . . . . 7
|
202 | | prcom 4267 |
. . . . . . . . 9
|
203 | 202 | eleq1i 2692 |
. . . . . . . 8
|
204 | | prcom 4267 |
. . . . . . . . 9
|
205 | 204 | eleq1i 2692 |
. . . . . . . 8
|
206 | | biid 251 |
. . . . . . . 8
|
207 | 203, 205,
206 | 3anbi123i 1251 |
. . . . . . 7
|
208 | 200, 201,
207 | 3bitr3i 290 |
. . . . . 6
|
209 | | df-3an 1039 |
. . . . . . 7
|
210 | | biid 251 |
. . . . . . . 8
|
211 | | prcom 4267 |
. . . . . . . . 9
|
212 | 211 | eleq1i 2692 |
. . . . . . . 8
|
213 | 210, 205,
212 | 3anbi123i 1251 |
. . . . . . 7
|
214 | 209, 213 | bitr3i 266 |
. . . . . 6
|
215 | | df-3an 1039 |
. . . . . . 7
|
216 | | 3anrot 1043 |
. . . . . . . 8
|
217 | | 3anrot 1043 |
. . . . . . . 8
|
218 | | biid 251 |
. . . . . . . . 9
|
219 | 203, 218,
212 | 3anbi123i 1251 |
. . . . . . . 8
|
220 | 216, 217,
219 | 3bitri 286 |
. . . . . . 7
|
221 | 215, 220 | bitr3i 266 |
. . . . . 6
|
222 | 208, 214,
221 | 3anbi123i 1251 |
. . . . 5
|
223 | | df-3an 1039 |
. . . . . 6
|
224 | | anabs1 850 |
. . . . . 6
|
225 | | anidm 676 |
. . . . . 6
|
226 | 223, 224,
225 | 3bitri 286 |
. . . . 5
|
227 | 199, 222,
226 | 3bitri 286 |
. . . 4
|
228 | 180, 227 | syl6bb 276 |
. . 3
USGraph
|
229 | 13, 98, 228 | 3bitrd 294 |
. 2
USGraph
FriendGraph
|
230 | 229 | ex 450 |
1
USGraph FriendGraph
|