Step | Hyp | Ref
| Expression |
1 | | brsegle 32215 |
. 2
Cgr |
2 | | simprl 794 |
. . . . . . . 8
Cgr |
3 | | simpl1 1064 |
. . . . . . . . . 10
|
4 | | simpl3l 1116 |
. . . . . . . . . 10
|
5 | | simpl3r 1117 |
. . . . . . . . . 10
|
6 | | simpr 477 |
. . . . . . . . . 10
|
7 | | btwncolinear2 32177 |
. . . . . . . . . 10
|
8 | 3, 4, 5, 6, 7 | syl13anc 1328 |
. . . . . . . . 9
|
9 | 8 | adantr 481 |
. . . . . . . 8
Cgr
|
10 | 2, 9 | mpd 15 |
. . . . . . 7
Cgr |
11 | | simpl2l 1114 |
. . . . . . . 8
|
12 | | simpl2r 1115 |
. . . . . . . 8
|
13 | | simprr 796 |
. . . . . . . 8
Cgr Cgr |
14 | 3, 11, 12, 4, 6, 13 | cgrcomand 32098 |
. . . . . . 7
Cgr Cgr |
15 | | simpl2 1065 |
. . . . . . . . 9
|
16 | | lineext 32183 |
. . . . . . . . 9
Cgr Cgr3 |
17 | 3, 4, 6, 5, 15, 16 | syl131anc 1339 |
. . . . . . . 8
Cgr Cgr3 |
18 | 17 | adantr 481 |
. . . . . . 7
Cgr
Cgr
Cgr3 |
19 | 10, 14, 18 | mp2and 715 |
. . . . . 6
Cgr Cgr3 |
20 | | an32 839 |
. . . . . . . . 9
|
21 | | simpll1 1100 |
. . . . . . . . . . . 12
|
22 | | simpl3l 1116 |
. . . . . . . . . . . . 13
|
23 | 22 | adantr 481 |
. . . . . . . . . . . 12
|
24 | | simpr 477 |
. . . . . . . . . . . 12
|
25 | | simpl3r 1117 |
. . . . . . . . . . . . 13
|
26 | 25 | adantr 481 |
. . . . . . . . . . . 12
|
27 | | simpl2l 1114 |
. . . . . . . . . . . . 13
|
28 | 27 | adantr 481 |
. . . . . . . . . . . 12
|
29 | | simpl2r 1115 |
. . . . . . . . . . . . 13
|
30 | 29 | adantr 481 |
. . . . . . . . . . . 12
|
31 | | simplr 792 |
. . . . . . . . . . . 12
|
32 | | brcgr3 32153 |
. . . . . . . . . . . 12
Cgr3
Cgr
Cgr Cgr |
33 | 21, 23, 24, 26, 28, 30, 31, 32 | syl133anc 1349 |
. . . . . . . . . . 11
Cgr3 Cgr Cgr
Cgr
|
34 | 33 | adantr 481 |
. . . . . . . . . 10
Cgr Cgr3
Cgr
Cgr Cgr |
35 | | simp2l 1087 |
. . . . . . . . . . . . 13
Cgr
Cgr Cgr
Cgr
|
36 | | simp3 1063 |
. . . . . . . . . . . . . 14
Cgr
Cgr Cgr
Cgr
Cgr
Cgr Cgr |
37 | 33 | 3ad2ant1 1082 |
. . . . . . . . . . . . . 14
Cgr
Cgr Cgr
Cgr
Cgr3
Cgr
Cgr Cgr |
38 | 36, 37 | mpbird 247 |
. . . . . . . . . . . . 13
Cgr
Cgr Cgr
Cgr
Cgr3
|
39 | | btwnxfr 32163 |
. . . . . . . . . . . . . . 15
Cgr3
|
40 | 21, 23, 24, 26, 28, 30, 31, 39 | syl133anc 1349 |
. . . . . . . . . . . . . 14
Cgr3
|
41 | 40 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
Cgr
Cgr Cgr
Cgr
Cgr3
|
42 | 35, 38, 41 | mp2and 715 |
. . . . . . . . . . . 12
Cgr
Cgr Cgr
Cgr
|
43 | | simp32 1098 |
. . . . . . . . . . . . 13
Cgr
Cgr Cgr
Cgr
Cgr |
44 | | cgrcom 32097 |
. . . . . . . . . . . . . . 15
Cgr Cgr
|
45 | 21, 23, 26, 28, 31, 44 | syl122anc 1335 |
. . . . . . . . . . . . . 14
Cgr Cgr |
46 | 45 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
Cgr
Cgr Cgr
Cgr
Cgr Cgr
|
47 | 43, 46 | mpbid 222 |
. . . . . . . . . . . 12
Cgr
Cgr Cgr
Cgr
Cgr |
48 | 42, 47 | jca 554 |
. . . . . . . . . . 11
Cgr
Cgr Cgr
Cgr
Cgr |
49 | 48 | 3expia 1267 |
. . . . . . . . . 10
Cgr Cgr Cgr Cgr
Cgr
|
50 | 34, 49 | sylbid 230 |
. . . . . . . . 9
Cgr Cgr3 Cgr |
51 | 20, 50 | sylanb 489 |
. . . . . . . 8
Cgr Cgr3 Cgr |
52 | 51 | an32s 846 |
. . . . . . 7
Cgr Cgr3 Cgr |
53 | 52 | reximdva 3017 |
. . . . . 6
Cgr
Cgr3
Cgr
|
54 | 19, 53 | mpd 15 |
. . . . 5
Cgr
Cgr
|
55 | 54 | ex 450 |
. . . 4
Cgr
Cgr |
56 | 55 | rexlimdva 3031 |
. . 3
Cgr
Cgr |
57 | | simprl 794 |
. . . . . . . 8
Cgr |
58 | | simpll1 1100 |
. . . . . . . . 9
Cgr |
59 | 27 | adantr 481 |
. . . . . . . . 9
Cgr |
60 | | simplr 792 |
. . . . . . . . 9
Cgr |
61 | 29 | adantr 481 |
. . . . . . . . 9
Cgr |
62 | | btwncolinear1 32176 |
. . . . . . . . 9
|
63 | 58, 59, 60, 61, 62 | syl13anc 1328 |
. . . . . . . 8
Cgr |
64 | 57, 63 | mpd 15 |
. . . . . . 7
Cgr |
65 | | simprr 796 |
. . . . . . 7
Cgr Cgr |
66 | | simpl1 1064 |
. . . . . . . . 9
|
67 | | simpr 477 |
. . . . . . . . 9
|
68 | | simpl3 1066 |
. . . . . . . . 9
|
69 | | lineext 32183 |
. . . . . . . . 9
Cgr Cgr3 |
70 | 66, 27, 67, 29, 68, 69 | syl131anc 1339 |
. . . . . . . 8
Cgr Cgr3 |
71 | 70 | adantr 481 |
. . . . . . 7
Cgr
Cgr
Cgr3 |
72 | 64, 65, 71 | mp2and 715 |
. . . . . 6
Cgr Cgr3 |
73 | 27, 67, 29 | 3jca 1242 |
. . . . . . . . . . . 12
|
74 | 73 | adantr 481 |
. . . . . . . . . . 11
|
75 | | brcgr3 32153 |
. . . . . . . . . . 11
Cgr3
Cgr
Cgr Cgr |
76 | 21, 74, 23, 26, 24, 75 | syl113anc 1338 |
. . . . . . . . . 10
Cgr3 Cgr Cgr
Cgr
|
77 | 76 | adantr 481 |
. . . . . . . . 9
Cgr Cgr3
Cgr
Cgr Cgr |
78 | | simp2l 1087 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr
Cgr
|
79 | | simp32 1098 |
. . . . . . . . . . . . . 14
Cgr
Cgr
Cgr
Cgr
Cgr |
80 | | simp2r 1088 |
. . . . . . . . . . . . . 14
Cgr
Cgr
Cgr
Cgr
Cgr |
81 | | simp33 1099 |
. . . . . . . . . . . . . . 15
Cgr
Cgr
Cgr
Cgr
Cgr |
82 | | cgrcomlr 32105 |
. . . . . . . . . . . . . . . . 17
Cgr Cgr |
83 | 21, 31, 30, 26, 24, 82 | syl122anc 1335 |
. . . . . . . . . . . . . . . 16
Cgr
Cgr |
84 | 83 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
Cgr
Cgr
Cgr
Cgr
Cgr Cgr |
85 | 81, 84 | mpbid 222 |
. . . . . . . . . . . . . 14
Cgr
Cgr
Cgr
Cgr
Cgr |
86 | 79, 80, 85 | 3jca 1242 |
. . . . . . . . . . . . 13
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr Cgr |
87 | | brcgr3 32153 |
. . . . . . . . . . . . . . 15
Cgr3
Cgr
Cgr Cgr |
88 | 21, 28, 30, 31, 23, 24, 26, 87 | syl133anc 1349 |
. . . . . . . . . . . . . 14
Cgr3 Cgr
Cgr
Cgr |
89 | 88 | 3ad2ant1 1082 |
. . . . . . . . . . . . 13
Cgr
Cgr
Cgr
Cgr
Cgr3
Cgr
Cgr Cgr |
90 | 86, 89 | mpbird 247 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr
Cgr
Cgr3
|
91 | | btwnxfr 32163 |
. . . . . . . . . . . . . 14
Cgr3
|
92 | 21, 28, 30, 31, 23, 24, 26, 91 | syl133anc 1349 |
. . . . . . . . . . . . 13
Cgr3
|
93 | 92 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr
Cgr
Cgr3
|
94 | 78, 90, 93 | mp2and 715 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr
Cgr
|
95 | 94, 79 | jca 554 |
. . . . . . . . . 10
Cgr
Cgr
Cgr
Cgr
Cgr |
96 | 95 | 3expia 1267 |
. . . . . . . . 9
Cgr Cgr Cgr
Cgr
Cgr
|
97 | 77, 96 | sylbid 230 |
. . . . . . . 8
Cgr Cgr3
Cgr |
98 | 97 | an32s 846 |
. . . . . . 7
Cgr Cgr3
Cgr |
99 | 98 | reximdva 3017 |
. . . . . 6
Cgr
Cgr3
Cgr
|
100 | 72, 99 | mpd 15 |
. . . . 5
Cgr
Cgr
|
101 | 100 | ex 450 |
. . . 4
Cgr
Cgr |
102 | 101 | rexlimdva 3031 |
. . 3
Cgr
Cgr |
103 | 56, 102 | impbid 202 |
. 2
Cgr
Cgr |
104 | 1, 103 | bitrd 268 |
1
Cgr |