Step | Hyp | Ref
| Expression |
1 | | iscgra.p |
. . 3
|
2 | | eqid 2622 |
. . 3
LineG LineG |
3 | | iscgra.i |
. . 3
Itv |
4 | | iscgra.g |
. . . 4
TarskiG |
5 | 4 | ad3antrrr 766 |
. . 3
cgrG TarskiG |
6 | | iscgra.a |
. . . 4
|
7 | 6 | ad3antrrr 766 |
. . 3
cgrG |
8 | | iscgra.b |
. . . 4
|
9 | 8 | ad3antrrr 766 |
. . 3
cgrG |
10 | | cgrahl1.x |
. . . 4
|
11 | 10 | ad3antrrr 766 |
. . 3
cgrG |
12 | | eqid 2622 |
. . 3
cgrG cgrG |
13 | | simpllr 799 |
. . 3
cgrG |
14 | | iscgra.e |
. . . 4
|
15 | 14 | ad3antrrr 766 |
. . 3
cgrG |
16 | | cgracgr.m |
. . 3
|
17 | | cgracgr.y |
. . . 4
|
18 | 17 | ad3antrrr 766 |
. . 3
cgrG |
19 | | iscgra.d |
. . . 4
|
20 | 19 | ad3antrrr 766 |
. . 3
cgrG |
21 | | iscgra.f |
. . . 4
|
22 | 21 | ad3antrrr 766 |
. . 3
cgrG |
23 | | iscgra.k |
. . . . . . . . 9
hlG |
24 | | iscgra.c |
. . . . . . . . 9
|
25 | | cgrahl1.2 |
. . . . . . . . 9
cgrA |
26 | 1, 3, 23, 4, 6, 8,
24, 19, 14, 21, 25 | cgrane1 25704 |
. . . . . . . 8
|
27 | 26 | necomd 2849 |
. . . . . . 7
|
28 | | cgracgr.1 |
. . . . . . . 8
|
29 | 1, 3, 23, 10, 6, 8, 4, 2, 28 | hlln 25502 |
. . . . . . 7
LineG |
30 | 1, 3, 2, 4, 8, 6, 10, 27, 29 | lncom 25517 |
. . . . . 6
LineG |
31 | 30 | orcd 407 |
. . . . 5
LineG |
32 | 1, 2, 3, 4, 8, 6, 10, 31 | colrot1 25454 |
. . . 4
LineG |
33 | 32 | ad3antrrr 766 |
. . 3
cgrG LineG |
34 | 24 | ad3antrrr 766 |
. . . . 5
cgrG |
35 | | simplr 792 |
. . . . 5
cgrG |
36 | | simpr1 1067 |
. . . . 5
cgrG cgrG |
37 | 1, 16, 3, 12, 5, 7,
9, 34, 13, 15, 35, 36 | cgr3simp1 25415 |
. . . 4
cgrG |
38 | | cgracgr.3 |
. . . . 5
|
39 | 38 | ad3antrrr 766 |
. . . 4
cgrG |
40 | | eqid 2622 |
. . . . . . 7
≤G ≤G |
41 | | simpr2 1068 |
. . . . . . . . 9
cgrG |
42 | 1, 3, 23, 13, 20, 15, 5 | ishlg 25497 |
. . . . . . . . 9
cgrG
|
43 | 41, 42 | mpbid 222 |
. . . . . . . 8
cgrG
|
44 | 43 | simp3d 1075 |
. . . . . . 7
cgrG |
45 | 1, 3, 23, 10, 6, 8, 4 | ishlg 25497 |
. . . . . . . . . . 11
|
46 | 28, 45 | mpbid 222 |
. . . . . . . . . 10
|
47 | 46 | simp3d 1075 |
. . . . . . . . 9
|
48 | 47 | orcomd 403 |
. . . . . . . 8
|
49 | 48 | ad3antrrr 766 |
. . . . . . 7
cgrG |
50 | 37 | eqcomd 2628 |
. . . . . . . 8
cgrG |
51 | 1, 16, 3, 5, 13, 15, 7, 9, 50 | tgcgrcomlr 25375 |
. . . . . . 7
cgrG |
52 | 39 | eqcomd 2628 |
. . . . . . 7
cgrG |
53 | 1, 16, 3, 40, 5, 15, 13, 20, 9, 9, 7, 11,
44, 49, 51, 52 | tgcgrsub2 25490 |
. . . . . 6
cgrG |
54 | 53 | eqcomd 2628 |
. . . . 5
cgrG |
55 | 1, 16, 3, 5, 7, 11,
13, 20, 54 | tgcgrcomlr 25375 |
. . . 4
cgrG |
56 | 1, 16, 12, 5, 7, 9,
11, 13, 15, 20, 37, 39, 55 | trgcgr 25411 |
. . 3
cgrG cgrG |
57 | | cgracgr.2 |
. . . . . . . . 9
|
58 | 1, 3, 23, 17, 24, 8, 4, 2, 57 | hlln 25502 |
. . . . . . . 8
LineG |
59 | 58 | orcd 407 |
. . . . . . 7
LineG |
60 | 1, 2, 3, 4, 24, 8,
17, 59 | colrot1 25454 |
. . . . . 6
LineG |
61 | 60 | ad3antrrr 766 |
. . . . 5
cgrG LineG |
62 | 1, 16, 3, 12, 5, 7,
9, 34, 13, 15, 35, 36 | cgr3simp2 25416 |
. . . . . 6
cgrG |
63 | 1, 3, 23, 17, 24, 8, 4 | ishlg 25497 |
. . . . . . . . . . 11
|
64 | 57, 63 | mpbid 222 |
. . . . . . . . . 10
|
65 | 64 | simp3d 1075 |
. . . . . . . . 9
|
66 | 65 | orcomd 403 |
. . . . . . . 8
|
67 | 66 | ad3antrrr 766 |
. . . . . . 7
cgrG |
68 | | simpr3 1069 |
. . . . . . . . 9
cgrG |
69 | 1, 3, 23, 35, 22, 15, 5 | ishlg 25497 |
. . . . . . . . 9
cgrG
|
70 | 68, 69 | mpbid 222 |
. . . . . . . 8
cgrG
|
71 | 70 | simp3d 1075 |
. . . . . . 7
cgrG |
72 | | cgracgr.4 |
. . . . . . . 8
|
73 | 72 | ad3antrrr 766 |
. . . . . . 7
cgrG |
74 | 1, 16, 3, 40, 5, 9,
34, 18, 15, 15, 35, 22, 67, 71, 62, 73 | tgcgrsub2 25490 |
. . . . . 6
cgrG |
75 | 1, 16, 3, 5, 9, 18,
15, 22, 73 | tgcgrcomlr 25375 |
. . . . . 6
cgrG |
76 | 1, 16, 12, 5, 9, 34, 18, 15, 35, 22, 62, 74, 75 | trgcgr 25411 |
. . . . 5
cgrG cgrG |
77 | 51 | eqcomd 2628 |
. . . . 5
cgrG |
78 | 1, 16, 3, 12, 5, 7,
9, 34, 13, 15, 35, 36 | cgr3simp3 25417 |
. . . . 5
cgrG |
79 | 1, 3, 23, 4, 6, 8,
24, 19, 14, 21, 25 | cgrane2 25705 |
. . . . . 6
|
80 | 79 | ad3antrrr 766 |
. . . . 5
cgrG |
81 | 1, 2, 3, 5, 9, 34,
18, 12, 15, 35, 16, 7, 22, 13, 61, 76, 77, 78, 80 | tgfscgr 25463 |
. . . 4
cgrG |
82 | 1, 16, 3, 5, 18, 7,
22, 13, 81 | tgcgrcomlr 25375 |
. . 3
cgrG |
83 | 26 | ad3antrrr 766 |
. . 3
cgrG |
84 | 1, 2, 3, 5, 7, 9, 11, 12, 13, 15, 16, 18, 20, 22, 33, 56, 82, 73, 83 | tgfscgr 25463 |
. 2
cgrG |
85 | 1, 3, 23, 4, 6, 8,
24, 19, 14, 21 | iscgra 25701 |
. . 3
cgrA
cgrG |
86 | 25, 85 | mpbid 222 |
. 2
cgrG |
87 | 84, 86 | r19.29vva 3081 |
1
|