Description: Deduce equality from two right angles. Theorem 8.6 of Schwabhauser p. 58. (Contributed by Thierry Arnoux, 3-Sep-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | israg.p | |
|
israg.d | |
||
israg.i | |
||
israg.l | |
||
israg.s | |
||
israg.g | |
||
israg.a | |
||
israg.b | |
||
israg.c | |
||
ragflat2.d | |
||
ragflat2.1 | |
||
ragflat2.2 | |
||
ragflat2.3 | |
||
Assertion | ragflat2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | israg.p | |
|
2 | israg.d | |
|
3 | israg.i | |
|
4 | israg.l | |
|
5 | israg.s | |
|
6 | israg.g | |
|
7 | israg.a | |
|
8 | israg.b | |
|
9 | israg.c | |
|
10 | ragflat2.d | |
|
11 | ragflat2.1 | |
|
12 | ragflat2.2 | |
|
13 | ragflat2.3 | |
|
14 | eqid | |
|
15 | eqid | |
|
16 | 1 2 3 4 5 6 8 15 9 | mircl | |
17 | 1 2 3 4 5 6 7 8 9 | israg | |
18 | 11 17 | mpbid | |
19 | 1 2 3 4 5 6 10 8 9 | israg | |
20 | 12 19 | mpbid | |
21 | 1 4 3 6 7 10 9 14 16 7 2 13 18 20 | tgidinside | |
22 | 21 | eqcomd | |
23 | 1 2 3 4 5 6 8 15 9 | mirinv | |
24 | 22 23 | mpbid | |