Description: Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tkgeom.p | |
|
tkgeom.d | |
||
tkgeom.i | |
||
tkgeom.g | |
||
tgcgrcomlr.a | |
||
tgcgrcomlr.b | |
||
tgcgrcomlr.c | |
||
tgcgrcomlr.d | |
||
tgcgrcomlr.6 | |
||
Assertion | tgcgreqb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tkgeom.p | |
|
2 | tkgeom.d | |
|
3 | tkgeom.i | |
|
4 | tkgeom.g | |
|
5 | tgcgrcomlr.a | |
|
6 | tgcgrcomlr.b | |
|
7 | tgcgrcomlr.c | |
|
8 | tgcgrcomlr.d | |
|
9 | tgcgrcomlr.6 | |
|
10 | 4 | adantr | |
11 | 7 | adantr | |
12 | 8 | adantr | |
13 | 6 | adantr | |
14 | 9 | adantr | |
15 | simpr | |
|
16 | 15 | oveq1d | |
17 | 14 16 | eqtr3d | |
18 | 1 2 3 10 11 12 13 17 | axtgcgrid | |
19 | 4 | adantr | |
20 | 5 | adantr | |
21 | 6 | adantr | |
22 | 8 | adantr | |
23 | 9 | adantr | |
24 | simpr | |
|
25 | 24 | oveq1d | |
26 | 23 25 | eqtrd | |
27 | 1 2 3 19 20 21 22 26 | axtgcgrid | |
28 | 18 27 | impbida | |