Detailed syntax breakdown of Definition df-cgr3
Step | Hyp | Ref
| Expression |
1 | | ccgr3 25878 |
. 2
Cgr3 |
2 | | vp |
. . . . . . . . . . . . 13
 |
3 | 2 | cv 1648 |
. . . . . . . . . . . 12
 |
4 | | va |
. . . . . . . . . . . . . 14
 |
5 | 4 | cv 1648 |
. . . . . . . . . . . . 13
 |
6 | | vb |
. . . . . . . . . . . . . . 15
 |
7 | 6 | cv 1648 |
. . . . . . . . . . . . . 14
 |
8 | | vc |
. . . . . . . . . . . . . . 15
 |
9 | 8 | cv 1648 |
. . . . . . . . . . . . . 14
 |
10 | 7, 9 | cop 3781 |
. . . . . . . . . . . . 13
    |
11 | 5, 10 | cop 3781 |
. . . . . . . . . . . 12
       |
12 | 3, 11 | wceq 1649 |
. . . . . . . . . . 11
       |
13 | | vq |
. . . . . . . . . . . . 13
 |
14 | 13 | cv 1648 |
. . . . . . . . . . . 12
 |
15 | | vd |
. . . . . . . . . . . . . 14
 |
16 | 15 | cv 1648 |
. . . . . . . . . . . . 13
 |
17 | | ve |
. . . . . . . . . . . . . . 15
 |
18 | 17 | cv 1648 |
. . . . . . . . . . . . . 14
 |
19 | | vf |
. . . . . . . . . . . . . . 15
 |
20 | 19 | cv 1648 |
. . . . . . . . . . . . . 14
 |
21 | 18, 20 | cop 3781 |
. . . . . . . . . . . . 13
    |
22 | 16, 21 | cop 3781 |
. . . . . . . . . . . 12
       |
23 | 14, 22 | wceq 1649 |
. . . . . . . . . . 11
       |
24 | 5, 7 | cop 3781 |
. . . . . . . . . . . . 13
    |
25 | 16, 18 | cop 3781 |
. . . . . . . . . . . . 13
    |
26 | | ccgr 25737 |
. . . . . . . . . . . . 13
Cgr |
27 | 24, 25, 26 | wbr 4176 |
. . . . . . . . . . . 12
   Cgr    |
28 | 5, 9 | cop 3781 |
. . . . . . . . . . . . 13
    |
29 | 16, 20 | cop 3781 |
. . . . . . . . . . . . 13
    |
30 | 28, 29, 26 | wbr 4176 |
. . . . . . . . . . . 12
   Cgr    |
31 | 10, 21, 26 | wbr 4176 |
. . . . . . . . . . . 12
   Cgr    |
32 | 27, 30, 31 | w3a 936 |
. . . . . . . . . . 11
    Cgr      Cgr      Cgr     |
33 | 12, 23, 32 | w3a 936 |
. . . . . . . . . 10
                 Cgr      Cgr      Cgr      |
34 | | vn |
. . . . . . . . . . . 12
 |
35 | 34 | cv 1648 |
. . . . . . . . . . 11
 |
36 | | cee 25735 |
. . . . . . . . . . 11
 |
37 | 35, 36 | cfv 5417 |
. . . . . . . . . 10
     |
38 | 33, 19, 37 | wrex 2671 |
. . . . . . . . 9
                       Cgr      Cgr      Cgr      |
39 | 38, 17, 37 | wrex 2671 |
. . . . . . . 8
                             Cgr      Cgr      Cgr      |
40 | 39, 15, 37 | wrex 2671 |
. . . . . . 7
                                   Cgr      Cgr      Cgr      |
41 | 40, 8, 37 | wrex 2671 |
. . . . . 6
                                         Cgr      Cgr      Cgr      |
42 | 41, 6, 37 | wrex 2671 |
. . . . 5
                                               Cgr      Cgr      Cgr      |
43 | 42, 4, 37 | wrex 2671 |
. . . 4
                                                     Cgr      Cgr      Cgr      |
44 | | cn 9960 |
. . . 4
 |
45 | 43, 34, 44 | wrex 2671 |
. . 3
                                                      Cgr      Cgr      Cgr      |
46 | 45, 2, 13 | copab 4229 |
. 2
    
                                                     Cgr      Cgr      Cgr       |
47 | 1, 46 | wceq 1649 |
1
Cgr3                                                
          Cgr      Cgr      Cgr       |