Step |
Hyp |
Ref |
Expression |
1 |
|
dfcgra2.p |
|
2 |
|
dfcgra2.i |
|
3 |
|
dfcgra2.m |
|
4 |
|
dfcgra2.g |
|
5 |
|
dfcgra2.a |
|
6 |
|
dfcgra2.b |
|
7 |
|
dfcgra2.c |
|
8 |
|
dfcgra2.d |
|
9 |
|
dfcgra2.e |
|
10 |
|
dfcgra2.f |
|
11 |
|
eqid |
|
12 |
4
|
adantr |
|
13 |
5
|
adantr |
|
14 |
6
|
adantr |
|
15 |
7
|
adantr |
|
16 |
8
|
adantr |
|
17 |
9
|
adantr |
|
18 |
10
|
adantr |
|
19 |
|
simpr |
|
20 |
1 2 11 12 13 14 15 16 17 18 19
|
cgrane1 |
|
21 |
1 2 11 12 13 14 15 16 17 18 19
|
cgrane2 |
|
22 |
21
|
necomd |
|
23 |
20 22
|
jca |
|
24 |
1 2 11 12 13 14 15 16 17 18 19
|
cgrane3 |
|
25 |
24
|
necomd |
|
26 |
1 2 11 12 13 14 15 16 17 18 19
|
cgrane4 |
|
27 |
26
|
necomd |
|
28 |
25 27
|
jca |
|
29 |
|
simprl |
|
30 |
|
simprr |
|
31 |
4
|
ad6antr |
|
32 |
|
simp-5r |
|
33 |
6
|
ad6antr |
|
34 |
|
simp-4r |
|
35 |
|
simpllr |
|
36 |
9
|
ad6antr |
|
37 |
|
simplr |
|
38 |
10
|
ad6antr |
|
39 |
8
|
ad6antr |
|
40 |
7
|
ad6antr |
|
41 |
5
|
ad6antr |
|
42 |
|
simp-6r |
|
43 |
1 2 31 11 41 33 40 39 36 38 42
|
cgracom |
|
44 |
29
|
simplld |
|
45 |
20
|
ad5antr |
|
46 |
1 3 2 31 33 41 32 44 45
|
tgbtwnne |
|
47 |
1 2 11 33 32 41 31 41 44 46 45
|
btwnhl1 |
|
48 |
1 2 11 41 32 33 31 47
|
hlcomd |
|
49 |
1 2 11 31 39 36 38 41 33 40 43 32 48
|
cgrahl1 |
|
50 |
29
|
simprld |
|
51 |
22
|
ad5antr |
|
52 |
1 3 2 31 33 40 34 50 51
|
tgbtwnne |
|
53 |
1 2 11 33 34 40 31 41 50 52 51
|
btwnhl1 |
|
54 |
1 2 11 40 34 33 31 53
|
hlcomd |
|
55 |
1 2 11 31 39 36 38 32 33 40 49 34 54
|
cgrahl2 |
|
56 |
1 2 31 11 39 36 38 32 33 34 55
|
cgracom |
|
57 |
30
|
simplld |
|
58 |
25
|
ad5antr |
|
59 |
1 3 2 31 36 39 35 57 58
|
tgbtwnne |
|
60 |
1 2 11 36 35 39 31 41 57 59 58
|
btwnhl1 |
|
61 |
1 2 11 39 35 36 31 60
|
hlcomd |
|
62 |
1 2 11 31 32 33 34 39 36 38 56 35 61
|
cgrahl1 |
|
63 |
30
|
simprld |
|
64 |
27
|
ad5antr |
|
65 |
1 3 2 31 36 38 37 63 64
|
tgbtwnne |
|
66 |
1 2 11 36 37 38 31 41 63 65 64
|
btwnhl1 |
|
67 |
1 2 11 38 37 36 31 66
|
hlcomd |
|
68 |
1 2 11 31 32 33 34 35 36 38 62 37 67
|
cgrahl2 |
|
69 |
46
|
necomd |
|
70 |
1 2 11 32 41 33 31 69
|
hlid |
|
71 |
52
|
necomd |
|
72 |
1 2 11 34 41 33 31 71
|
hlid |
|
73 |
1 3 2 31 33 41 32 44
|
tgbtwncom |
|
74 |
29
|
simplrd |
|
75 |
1 3 2 31 41 32 36 39 74
|
tgcgrcoml |
|
76 |
30
|
simplrd |
|
77 |
76
|
eqcomd |
|
78 |
1 3 2 31 33 41 39 35 77
|
tgcgrcoml |
|
79 |
1 3 2 31 32 41 33 36 39 35 73 57 75 78
|
tgcgrextend |
|
80 |
1 3 2 31 32 33 36 35 79
|
tgcgrcoml |
|
81 |
1 3 2 31 33 40 34 50
|
tgbtwncom |
|
82 |
29
|
simprrd |
|
83 |
1 3 2 31 40 34 36 38 82
|
tgcgrcoml |
|
84 |
30
|
simprrd |
|
85 |
84
|
eqcomd |
|
86 |
1 3 2 31 33 40 38 37 85
|
tgcgrcoml |
|
87 |
1 3 2 31 34 40 33 36 38 37 81 63 83 86
|
tgcgrextend |
|
88 |
1 3 2 31 34 33 36 37 87
|
tgcgrcoml |
|
89 |
1 2 11 31 32 33 34 35 36 37 68 32 3 34 70 72 80 88
|
cgracgr |
|
90 |
29 30 89
|
3jca |
|
91 |
90
|
ex |
|
92 |
91
|
reximdva |
|
93 |
92
|
reximdva |
|
94 |
93
|
imp |
|
95 |
1 3 2 4 6 5 9 8
|
axtgsegcon |
|
96 |
1 3 2 4 6 7 9 10
|
axtgsegcon |
|
97 |
|
reeanv |
|
98 |
95 96 97
|
sylanbrc |
|
99 |
1 3 2 4 9 8 6 5
|
axtgsegcon |
|
100 |
1 3 2 4 9 10 6 7
|
axtgsegcon |
|
101 |
|
reeanv |
|
102 |
99 100 101
|
sylanbrc |
|
103 |
98 102
|
jca |
|
104 |
|
r19.41vv |
|
105 |
|
ancom |
|
106 |
105
|
2rexbii |
|
107 |
|
ancom |
|
108 |
104 106 107
|
3bitr3i |
|
109 |
108
|
2rexbii |
|
110 |
|
r19.41vv |
|
111 |
109 110
|
bitr2i |
|
112 |
103 111
|
sylib |
|
113 |
112
|
adantr |
|
114 |
94 113
|
reximddv2 |
|
115 |
23 28 114
|
3jca |
|
116 |
|
df-3an |
|
117 |
4
|
ad6antr |
|
118 |
8
|
ad6antr |
|
119 |
9
|
ad6antr |
|
120 |
10
|
ad6antr |
|
121 |
5
|
ad6antr |
|
122 |
6
|
ad6antr |
|
123 |
7
|
ad6antr |
|
124 |
|
simp-4r |
|
125 |
|
simp-5r |
|
126 |
|
simpllr |
|
127 |
|
simplr |
|
128 |
|
eqid |
|
129 |
|
simpr1 |
|
130 |
129
|
simplld |
|
131 |
|
simpr2 |
|
132 |
131
|
simplld |
|
133 |
1 3 2 117 119 118 126 132
|
tgbtwncom |
|
134 |
131
|
simplrd |
|
135 |
134
|
eqcomd |
|
136 |
1 3 2 117 122 121 118 126 135
|
tgcgrcomr |
|
137 |
129
|
simplrd |
|
138 |
1 3 2 117 121 125 119 118 137
|
tgcgrcomr |
|
139 |
1 3 2 117 122 121 125 126 118 119 130 133 136 138
|
tgcgrextend |
|
140 |
1 3 2 117 122 125 126 119 139
|
tgcgrcoml |
|
141 |
129
|
simprld |
|
142 |
1 3 2 117 122 123 124 141
|
tgbtwncom |
|
143 |
131
|
simprld |
|
144 |
129
|
simprrd |
|
145 |
1 3 2 117 123 124 119 120 144
|
tgcgrcoml |
|
146 |
131
|
simprrd |
|
147 |
146
|
eqcomd |
|
148 |
1 3 2 117 122 123 120 127 147
|
tgcgrcoml |
|
149 |
1 3 2 117 124 123 122 119 120 127 142 143 145 148
|
tgcgrextend |
|
150 |
1 3 2 117 124 122 119 127 149
|
tgcgrcoml |
|
151 |
|
simpr3 |
|
152 |
1 3 2 117 125 124 126 127 151
|
tgcgrcomlr |
|
153 |
1 3 128 117 125 122 124 126 119 127 140 150 152
|
trgcgr |
|
154 |
|
simp-6r |
|
155 |
154
|
simprld |
|
156 |
1 3 2 117 119 118 126 132 155
|
tgbtwnne |
|
157 |
1 2 11 119 126 118 117 122 132 156 155
|
btwnhl1 |
|
158 |
1 2 11 118 126 119 117 157
|
hlcomd |
|
159 |
154
|
simprrd |
|
160 |
1 3 2 117 119 120 127 143 159
|
tgbtwnne |
|
161 |
1 2 11 119 127 120 117 122 143 160 159
|
btwnhl1 |
|
162 |
1 2 11 120 127 119 117 161
|
hlcomd |
|
163 |
1 2 11 117 125 122 124 118 119 120 126 127 153 158 162
|
iscgrad |
|
164 |
1 2 117 11 125 122 124 118 119 120 163
|
cgracom |
|
165 |
154
|
simplld |
|
166 |
1 3 2 117 122 121 125 130 165
|
tgbtwnne |
|
167 |
1 2 11 122 125 121 117 121 130 166 165
|
btwnhl1 |
|
168 |
1 2 11 117 118 119 120 125 122 124 164 121 167
|
cgrahl1 |
|
169 |
154
|
simplrd |
|
170 |
1 3 2 117 122 123 124 141 169
|
tgbtwnne |
|
171 |
1 2 11 122 124 123 117 121 141 170 169
|
btwnhl1 |
|
172 |
1 2 11 117 118 119 120 121 122 124 168 123 171
|
cgrahl2 |
|
173 |
1 2 117 11 118 119 120 121 122 123 172
|
cgracom |
|
174 |
173
|
adantl3r |
|
175 |
|
simpr |
|
176 |
|
oveq2 |
|
177 |
176
|
eleq2d |
|
178 |
|
oveq2 |
|
179 |
178
|
eqeq1d |
|
180 |
177 179
|
anbi12d |
|
181 |
180
|
anbi1d |
|
182 |
|
oveq1 |
|
183 |
182
|
eqeq2d |
|
184 |
181 183
|
3anbi23d |
|
185 |
|
oveq2 |
|
186 |
185
|
eleq2d |
|
187 |
|
oveq2 |
|
188 |
187
|
eqeq1d |
|
189 |
186 188
|
anbi12d |
|
190 |
189
|
anbi2d |
|
191 |
|
oveq2 |
|
192 |
191
|
eqeq2d |
|
193 |
190 192
|
3anbi23d |
|
194 |
184 193
|
cbvrex2vw |
|
195 |
175 194
|
sylib |
|
196 |
174 195
|
r19.29vva |
|
197 |
196
|
adantl3r |
|
198 |
|
simpr |
|
199 |
|
oveq2 |
|
200 |
199
|
eleq2d |
|
201 |
|
oveq2 |
|
202 |
201
|
eqeq1d |
|
203 |
200 202
|
anbi12d |
|
204 |
203
|
anbi1d |
|
205 |
|
oveq1 |
|
206 |
205
|
eqeq1d |
|
207 |
204 206
|
3anbi13d |
|
208 |
207
|
2rexbidv |
|
209 |
|
oveq2 |
|
210 |
209
|
eleq2d |
|
211 |
|
oveq2 |
|
212 |
211
|
eqeq1d |
|
213 |
210 212
|
anbi12d |
|
214 |
213
|
anbi2d |
|
215 |
|
oveq2 |
|
216 |
215
|
eqeq1d |
|
217 |
214 216
|
3anbi13d |
|
218 |
217
|
2rexbidv |
|
219 |
208 218
|
cbvrex2vw |
|
220 |
198 219
|
sylib |
|
221 |
197 220
|
r19.29vva |
|
222 |
221
|
anasss |
|
223 |
116 222
|
sylan2b |
|
224 |
115 223
|
impbida |
|