Description: Angle congruence preserves flat angles. Part of Theorem 11.21 of Schwabhauser p. 97. (Contributed by Thierry Arnoux, 9-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cgracol.p | |
|
cgracol.i | |
||
cgracol.m | |
||
cgracol.g | |
||
cgracol.a | |
||
cgracol.b | |
||
cgracol.c | |
||
cgracol.d | |
||
cgracol.e | |
||
cgracol.f | |
||
cgracol.1 | |
||
cgrabtwn.2 | |
||
Assertion | cgrabtwn | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cgracol.p | |
|
2 | cgracol.i | |
|
3 | cgracol.m | |
|
4 | cgracol.g | |
|
5 | cgracol.a | |
|
6 | cgracol.b | |
|
7 | cgracol.c | |
|
8 | cgracol.d | |
|
9 | cgracol.e | |
|
10 | cgracol.f | |
|
11 | cgracol.1 | |
|
12 | cgrabtwn.2 | |
|
13 | eqid | |
|
14 | simpllr | |
|
15 | 8 | ad3antrrr | |
16 | 10 | ad3antrrr | |
17 | 4 | ad3antrrr | |
18 | 9 | ad3antrrr | |
19 | simpr2 | |
|
20 | simplr | |
|
21 | simpr3 | |
|
22 | eqid | |
|
23 | 5 | ad3antrrr | |
24 | 6 | ad3antrrr | |
25 | 7 | ad3antrrr | |
26 | simpr1 | |
|
27 | 12 | ad3antrrr | |
28 | 1 3 2 22 17 23 24 25 14 18 20 26 27 | tgbtwnxfr | |
29 | 1 3 2 17 14 18 20 28 | tgbtwncom | |
30 | 1 2 13 20 16 14 17 18 21 29 | btwnhl | |
31 | 1 3 2 17 16 18 14 30 | tgbtwncom | |
32 | 1 2 13 14 15 16 17 18 19 31 | btwnhl | |
33 | 1 2 13 4 5 6 7 8 9 10 | iscgra | |
34 | 11 33 | mpbid | |
35 | 32 34 | r19.29vva | |