Detailed syntax breakdown of Definition df-cgr3
Step | Hyp | Ref
| Expression |
1 | | ccgr3 32143 |
. 2
Cgr3 |
2 | | vp |
. . . . . . . . . . . . 13
|
3 | 2 | cv 1482 |
. . . . . . . . . . . 12
|
4 | | va |
. . . . . . . . . . . . . 14
|
5 | 4 | cv 1482 |
. . . . . . . . . . . . 13
|
6 | | vb |
. . . . . . . . . . . . . . 15
|
7 | 6 | cv 1482 |
. . . . . . . . . . . . . 14
|
8 | | vc |
. . . . . . . . . . . . . . 15
|
9 | 8 | cv 1482 |
. . . . . . . . . . . . . 14
|
10 | 7, 9 | cop 4183 |
. . . . . . . . . . . . 13
|
11 | 5, 10 | cop 4183 |
. . . . . . . . . . . 12
|
12 | 3, 11 | wceq 1483 |
. . . . . . . . . . 11
|
13 | | vq |
. . . . . . . . . . . . 13
|
14 | 13 | cv 1482 |
. . . . . . . . . . . 12
|
15 | | vd |
. . . . . . . . . . . . . 14
|
16 | 15 | cv 1482 |
. . . . . . . . . . . . 13
|
17 | | ve |
. . . . . . . . . . . . . . 15
|
18 | 17 | cv 1482 |
. . . . . . . . . . . . . 14
|
19 | | vf |
. . . . . . . . . . . . . . 15
|
20 | 19 | cv 1482 |
. . . . . . . . . . . . . 14
|
21 | 18, 20 | cop 4183 |
. . . . . . . . . . . . 13
|
22 | 16, 21 | cop 4183 |
. . . . . . . . . . . 12
|
23 | 14, 22 | wceq 1483 |
. . . . . . . . . . 11
|
24 | 5, 7 | cop 4183 |
. . . . . . . . . . . . 13
|
25 | 16, 18 | cop 4183 |
. . . . . . . . . . . . 13
|
26 | | ccgr 25770 |
. . . . . . . . . . . . 13
Cgr |
27 | 24, 25, 26 | wbr 4653 |
. . . . . . . . . . . 12
Cgr |
28 | 5, 9 | cop 4183 |
. . . . . . . . . . . . 13
|
29 | 16, 20 | cop 4183 |
. . . . . . . . . . . . 13
|
30 | 28, 29, 26 | wbr 4653 |
. . . . . . . . . . . 12
Cgr |
31 | 10, 21, 26 | wbr 4653 |
. . . . . . . . . . . 12
Cgr |
32 | 27, 30, 31 | w3a 1037 |
. . . . . . . . . . 11
Cgr Cgr Cgr |
33 | 12, 23, 32 | w3a 1037 |
. . . . . . . . . 10
Cgr Cgr Cgr |
34 | | vn |
. . . . . . . . . . . 12
|
35 | 34 | cv 1482 |
. . . . . . . . . . 11
|
36 | | cee 25768 |
. . . . . . . . . . 11
|
37 | 35, 36 | cfv 5888 |
. . . . . . . . . 10
|
38 | 33, 19, 37 | wrex 2913 |
. . . . . . . . 9
Cgr Cgr Cgr |
39 | 38, 17, 37 | wrex 2913 |
. . . . . . . 8
Cgr Cgr Cgr |
40 | 39, 15, 37 | wrex 2913 |
. . . . . . 7
Cgr Cgr Cgr |
41 | 40, 8, 37 | wrex 2913 |
. . . . . 6
Cgr Cgr Cgr |
42 | 41, 6, 37 | wrex 2913 |
. . . . 5
Cgr Cgr Cgr |
43 | 42, 4, 37 | wrex 2913 |
. . . 4
Cgr Cgr Cgr |
44 | | cn 11020 |
. . . 4
|
45 | 43, 34, 44 | wrex 2913 |
. . 3
Cgr Cgr Cgr |
46 | 45, 2, 13 | copab 4712 |
. 2
Cgr Cgr Cgr |
47 | 1, 46 | wceq 1483 |
1
Cgr3
Cgr Cgr Cgr |