Step | Hyp | Ref
| Expression |
1 | | df-reu 2919 |
. . 3
|
2 | | eleq1 2689 |
. . . . . 6
|
3 | | preq1 4268 |
. . . . . . . 8
|
4 | | preq1 4268 |
. . . . . . . 8
|
5 | 3, 4 | preq12d 4276 |
. . . . . . 7
|
6 | 5 | sseq1d 3632 |
. . . . . 6
|
7 | 2, 6 | anbi12d 747 |
. . . . 5
|
8 | 7 | eu4 2518 |
. . . 4
|
9 | | frgr3v.v |
. . . . . . . 8
Vtx |
10 | | frgr3v.e |
. . . . . . . 8
Edg |
11 | 9, 10 | frgr3vlem1 27137 |
. . . . . . 7
USGraph
|
12 | 11 | 3expa 1265 |
. . . . . 6
USGraph
|
13 | 12 | biantrud 528 |
. . . . 5
USGraph
|
14 | | vex 3203 |
. . . . . . . . . . 11
|
15 | 14 | eltp 4230 |
. . . . . . . . . 10
|
16 | | preq1 4268 |
. . . . . . . . . . . . . 14
|
17 | | preq1 4268 |
. . . . . . . . . . . . . 14
|
18 | 16, 17 | preq12d 4276 |
. . . . . . . . . . . . 13
|
19 | 18 | sseq1d 3632 |
. . . . . . . . . . . 12
|
20 | | prex 4909 |
. . . . . . . . . . . . . 14
|
21 | | prex 4909 |
. . . . . . . . . . . . . 14
|
22 | 20, 21 | prss 4351 |
. . . . . . . . . . . . 13
|
23 | 10 | usgredgne 26098 |
. . . . . . . . . . . . . . . . . . 19
USGraph
|
24 | 23 | adantll 750 |
. . . . . . . . . . . . . . . . . 18
USGraph
|
25 | | df-ne 2795 |
. . . . . . . . . . . . . . . . . . 19
|
26 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
|
27 | 26 | pm2.24i 146 |
. . . . . . . . . . . . . . . . . . 19
|
28 | 25, 27 | sylbi 207 |
. . . . . . . . . . . . . . . . . 18
|
29 | 24, 28 | syl 17 |
. . . . . . . . . . . . . . . . 17
USGraph
|
30 | 29 | ex 450 |
. . . . . . . . . . . . . . . 16
USGraph
|
31 | 30 | adantl 482 |
. . . . . . . . . . . . . . 15
USGraph
|
32 | 31 | com12 32 |
. . . . . . . . . . . . . 14
USGraph
|
33 | 32 | adantr 481 |
. . . . . . . . . . . . 13
USGraph
|
34 | 22, 33 | sylbir 225 |
. . . . . . . . . . . 12
USGraph
|
35 | 19, 34 | syl6bi 243 |
. . . . . . . . . . 11
USGraph
|
36 | | preq1 4268 |
. . . . . . . . . . . . . 14
|
37 | | preq1 4268 |
. . . . . . . . . . . . . 14
|
38 | 36, 37 | preq12d 4276 |
. . . . . . . . . . . . 13
|
39 | 38 | sseq1d 3632 |
. . . . . . . . . . . 12
|
40 | | prex 4909 |
. . . . . . . . . . . . . 14
|
41 | | prex 4909 |
. . . . . . . . . . . . . 14
|
42 | 40, 41 | prss 4351 |
. . . . . . . . . . . . 13
|
43 | 10 | usgredgne 26098 |
. . . . . . . . . . . . . . . . . . 19
USGraph
|
44 | 43 | adantll 750 |
. . . . . . . . . . . . . . . . . 18
USGraph
|
45 | | df-ne 2795 |
. . . . . . . . . . . . . . . . . . 19
|
46 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . 20
|
47 | 46 | pm2.24i 146 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 45, 47 | sylbi 207 |
. . . . . . . . . . . . . . . . . 18
|
49 | 44, 48 | syl 17 |
. . . . . . . . . . . . . . . . 17
USGraph
|
50 | 49 | ex 450 |
. . . . . . . . . . . . . . . 16
USGraph
|
51 | 50 | adantl 482 |
. . . . . . . . . . . . . . 15
USGraph
|
52 | 51 | com12 32 |
. . . . . . . . . . . . . 14
USGraph
|
53 | 52 | adantl 482 |
. . . . . . . . . . . . 13
USGraph
|
54 | 42, 53 | sylbir 225 |
. . . . . . . . . . . 12
USGraph
|
55 | 39, 54 | syl6bi 243 |
. . . . . . . . . . 11
USGraph
|
56 | | preq1 4268 |
. . . . . . . . . . . . . 14
|
57 | | preq1 4268 |
. . . . . . . . . . . . . 14
|
58 | 56, 57 | preq12d 4276 |
. . . . . . . . . . . . 13
|
59 | 58 | sseq1d 3632 |
. . . . . . . . . . . 12
|
60 | | prex 4909 |
. . . . . . . . . . . . . 14
|
61 | | prex 4909 |
. . . . . . . . . . . . . 14
|
62 | 60, 61 | prss 4351 |
. . . . . . . . . . . . 13
|
63 | | ax-1 6 |
. . . . . . . . . . . . 13
USGraph
|
64 | 62, 63 | sylbir 225 |
. . . . . . . . . . . 12
USGraph
|
65 | 59, 64 | syl6bi 243 |
. . . . . . . . . . 11
USGraph
|
66 | 35, 55, 65 | 3jaoi 1391 |
. . . . . . . . . 10
USGraph
|
67 | 15, 66 | sylbi 207 |
. . . . . . . . 9
USGraph
|
68 | 67 | imp 445 |
. . . . . . . 8
USGraph
|
69 | 68 | com12 32 |
. . . . . . 7
USGraph
|
70 | 69 | exlimdv 1861 |
. . . . . 6
USGraph
|
71 | | prssi 4353 |
. . . . . . . . . . 11
|
72 | 71 | adantl 482 |
. . . . . . . . . 10
USGraph
|
73 | 72 | 3mix3d 1238 |
. . . . . . . . 9
USGraph
|
74 | 19, 39, 59 | rextpg 4237 |
. . . . . . . . . 10
|
75 | 74 | ad3antrrr 766 |
. . . . . . . . 9
USGraph
|
76 | 73, 75 | mpbird 247 |
. . . . . . . 8
USGraph
|
77 | | df-rex 2918 |
. . . . . . . 8
|
78 | 76, 77 | sylib 208 |
. . . . . . 7
USGraph
|
79 | 78 | ex 450 |
. . . . . 6
USGraph
|
80 | 70, 79 | impbid 202 |
. . . . 5
USGraph
|
81 | 13, 80 | bitr3d 270 |
. . . 4
USGraph
|
82 | 8, 81 | syl5bb 272 |
. . 3
USGraph
|
83 | 1, 82 | syl5bb 272 |
. 2
USGraph
|
84 | 83 | ex 450 |
1
USGraph
|