Step | Hyp | Ref
| Expression |
1 | | cgraid.p |
. . . . 5
|
2 | | eqid 2622 |
. . . . 5
|
3 | | eqid 2622 |
. . . . 5
cgrG cgrG |
4 | | cgraid.g |
. . . . . 6
TarskiG |
5 | 4 | ad3antrrr 766 |
. . . . 5
TarskiG |
6 | | cgraid.a |
. . . . . 6
|
7 | 6 | ad3antrrr 766 |
. . . . 5
|
8 | | cgraid.b |
. . . . . 6
|
9 | 8 | ad3antrrr 766 |
. . . . 5
|
10 | | cgraid.c |
. . . . . 6
|
11 | 10 | ad3antrrr 766 |
. . . . 5
|
12 | | simpllr 799 |
. . . . 5
|
13 | | cgratr.i |
. . . . . 6
|
14 | 13 | ad3antrrr 766 |
. . . . 5
|
15 | | simplr 792 |
. . . . 5
|
16 | | cgraid.i |
. . . . . 6
Itv |
17 | | simprlr 803 |
. . . . . . 7
|
18 | 17 | eqcomd 2628 |
. . . . . 6
|
19 | 1, 2, 16, 5, 9, 7,
14, 12, 18 | tgcgrcomlr 25375 |
. . . . 5
|
20 | | simprrr 805 |
. . . . . 6
|
21 | 20 | eqcomd 2628 |
. . . . 5
|
22 | 5 | ad3antrrr 766 |
. . . . . . . 8
cgrG TarskiG |
23 | 7 | ad3antrrr 766 |
. . . . . . . 8
cgrG |
24 | 9 | ad3antrrr 766 |
. . . . . . . 8
cgrG |
25 | 11 | ad3antrrr 766 |
. . . . . . . 8
cgrG |
26 | | simpllr 799 |
. . . . . . . 8
cgrG |
27 | | cgracom.e |
. . . . . . . . 9
|
28 | 27 | ad6antr 772 |
. . . . . . . 8
cgrG |
29 | | simplr 792 |
. . . . . . . 8
cgrG |
30 | | simpr1 1067 |
. . . . . . . 8
cgrG cgrG |
31 | 1, 2, 16, 3, 22, 23, 24, 25, 26, 28, 29, 30 | cgr3simp3 25417 |
. . . . . . 7
cgrG |
32 | 12 | ad3antrrr 766 |
. . . . . . . 8
cgrG |
33 | 15 | ad3antrrr 766 |
. . . . . . . 8
cgrG |
34 | | cgraid.k |
. . . . . . . . 9
hlG |
35 | | cgracom.d |
. . . . . . . . . 10
|
36 | 35 | ad6antr 772 |
. . . . . . . . 9
cgrG |
37 | | cgracom.f |
. . . . . . . . . 10
|
38 | 37 | ad6antr 772 |
. . . . . . . . 9
cgrG |
39 | 14 | ad3antrrr 766 |
. . . . . . . . 9
cgrG |
40 | | cgratr.j |
. . . . . . . . . . 11
|
41 | 40 | ad6antr 772 |
. . . . . . . . . 10
cgrG |
42 | | cgratr.h |
. . . . . . . . . . . 12
|
43 | 42 | ad6antr 772 |
. . . . . . . . . . 11
cgrG |
44 | | cgratr.1 |
. . . . . . . . . . . 12
cgrA |
45 | 44 | ad6antr 772 |
. . . . . . . . . . 11
cgrG cgrA |
46 | | simprll 802 |
. . . . . . . . . . . 12
|
47 | 46 | ad3antrrr 766 |
. . . . . . . . . . 11
cgrG |
48 | 1, 16, 34, 22, 36, 28, 38, 43, 39, 41, 45, 32, 47 | cgrahl1 25708 |
. . . . . . . . . 10
cgrG cgrA |
49 | | simprrl 804 |
. . . . . . . . . . 11
|
50 | 49 | ad3antrrr 766 |
. . . . . . . . . 10
cgrG |
51 | 1, 16, 34, 22, 36, 28, 38, 32, 39, 41, 48, 33, 50 | cgrahl2 25709 |
. . . . . . . . 9
cgrG cgrA |
52 | | simpr2 1068 |
. . . . . . . . 9
cgrG |
53 | | simpr3 1069 |
. . . . . . . . 9
cgrG |
54 | 1, 2, 16, 3, 22, 23, 24, 25, 26, 28, 29, 30 | cgr3simp1 25415 |
. . . . . . . . . . . 12
cgrG |
55 | 54 | eqcomd 2628 |
. . . . . . . . . . 11
cgrG |
56 | 1, 2, 16, 22, 26, 28, 23, 24, 55 | tgcgrcomlr 25375 |
. . . . . . . . . 10
cgrG |
57 | 18 | ad3antrrr 766 |
. . . . . . . . . 10
cgrG |
58 | 56, 57 | eqtrd 2656 |
. . . . . . . . 9
cgrG |
59 | 1, 2, 16, 3, 22, 23, 24, 25, 26, 28, 29, 30 | cgr3simp2 25416 |
. . . . . . . . . . 11
cgrG |
60 | 59 | eqcomd 2628 |
. . . . . . . . . 10
cgrG |
61 | 21 | ad3antrrr 766 |
. . . . . . . . . 10
cgrG |
62 | 60, 61 | eqtrd 2656 |
. . . . . . . . 9
cgrG |
63 | 1, 16, 34, 22, 36, 28, 38, 32, 39, 33, 51, 26, 2, 29, 52, 53, 58, 62 | cgracgr 25710 |
. . . . . . . 8
cgrG |
64 | 1, 2, 16, 22, 26, 29, 32, 33, 63 | tgcgrcomlr 25375 |
. . . . . . 7
cgrG |
65 | 31, 64 | eqtrd 2656 |
. . . . . 6
cgrG |
66 | | cgracom.1 |
. . . . . . . 8
cgrA |
67 | 1, 16, 34, 4, 6, 8,
10, 35, 27, 37 | iscgra 25701 |
. . . . . . . 8
cgrA
cgrG |
68 | 66, 67 | mpbid 222 |
. . . . . . 7
cgrG |
69 | 68 | ad3antrrr 766 |
. . . . . 6
cgrG |
70 | 65, 69 | r19.29vva 3081 |
. . . . 5
|
71 | 1, 2, 3, 5, 7, 9, 11, 12, 14, 15, 19, 21, 70 | trgcgr 25411 |
. . . 4
cgrG |
72 | 71, 46, 49 | 3jca 1242 |
. . 3
cgrG |
73 | 1, 16, 34, 4, 35, 27, 37, 42, 13, 40, 44 | cgrane3 25706 |
. . . . . 6
|
74 | 73 | necomd 2849 |
. . . . 5
|
75 | 1, 16, 34, 4, 6, 8,
10, 35, 27, 37, 66 | cgrane1 25704 |
. . . . . 6
|
76 | 75 | necomd 2849 |
. . . . 5
|
77 | 1, 16, 34, 13, 8, 6, 4, 42, 2,
74, 76 | hlcgrex 25511 |
. . . 4
|
78 | 1, 16, 34, 4, 35, 27, 37, 42, 13, 40, 44 | cgrane4 25707 |
. . . . . 6
|
79 | 78 | necomd 2849 |
. . . . 5
|
80 | 1, 16, 34, 4, 6, 8,
10, 35, 27, 37, 66 | cgrane2 25705 |
. . . . 5
|
81 | 1, 16, 34, 13, 8, 10, 4, 40, 2, 79, 80 | hlcgrex 25511 |
. . . 4
|
82 | | reeanv 3107 |
. . . 4
|
83 | 77, 81, 82 | sylanbrc 698 |
. . 3
|
84 | 72, 83 | reximddv2 3020 |
. 2
cgrG |
85 | 1, 16, 34, 4, 6, 8,
10, 42, 13, 40 | iscgra 25701 |
. 2
cgrA
cgrG |
86 | 84, 85 | mpbird 247 |
1
cgrA |