Step | Hyp | Ref
| Expression |
1 | | brifs 32150 |
. 2
Cgr
Cgr
Cgr Cgr |
2 | | simp1l 1085 |
. . . . . 6
Cgr Cgr Cgr Cgr
|
3 | | simp11 1091 |
. . . . . . 7
|
4 | | simp13 1093 |
. . . . . . 7
|
5 | | simp21 1094 |
. . . . . . 7
|
6 | | axbtwnid 25819 |
. . . . . . 7
|
7 | 3, 4, 5, 6 | syl3anc 1326 |
. . . . . 6
|
8 | 2, 7 | syl5 34 |
. . . . 5
Cgr
Cgr
Cgr Cgr
|
9 | | simp2r 1088 |
. . . . . . . . 9
Cgr Cgr Cgr Cgr
Cgr |
10 | | simp3r 1090 |
. . . . . . . . 9
Cgr Cgr Cgr Cgr
Cgr |
11 | 9, 10 | jca 554 |
. . . . . . . 8
Cgr Cgr Cgr Cgr
Cgr
Cgr |
12 | | opeq2 4403 |
. . . . . . . . . . 11
|
13 | 12 | breq1d 4663 |
. . . . . . . . . 10
Cgr
Cgr |
14 | | opeq1 4402 |
. . . . . . . . . . 11
|
15 | 14 | breq1d 4663 |
. . . . . . . . . 10
Cgr
Cgr |
16 | 13, 15 | anbi12d 747 |
. . . . . . . . 9
Cgr Cgr
Cgr Cgr
|
17 | 16 | biimprd 238 |
. . . . . . . 8
Cgr Cgr
Cgr Cgr |
18 | 11, 17 | mpan9 486 |
. . . . . . 7
Cgr
Cgr
Cgr Cgr Cgr
Cgr
|
19 | | simp31 1097 |
. . . . . . . . . 10
|
20 | | simp32 1098 |
. . . . . . . . . 10
|
21 | | cgrid2 32110 |
. . . . . . . . . 10
Cgr
|
22 | 3, 4, 19, 20, 21 | syl13anc 1328 |
. . . . . . . . 9
Cgr
|
23 | | opeq1 4402 |
. . . . . . . . . . 11
|
24 | 23 | breq2d 4665 |
. . . . . . . . . 10
Cgr
Cgr |
25 | 24 | biimprd 238 |
. . . . . . . . 9
Cgr
Cgr
|
26 | 22, 25 | syl6 35 |
. . . . . . . 8
Cgr
Cgr Cgr
|
27 | 26 | impd 447 |
. . . . . . 7
Cgr Cgr
Cgr |
28 | 18, 27 | syl5 34 |
. . . . . 6
Cgr
Cgr
Cgr Cgr Cgr |
29 | 28 | expd 452 |
. . . . 5
Cgr
Cgr
Cgr Cgr
Cgr |
30 | 8, 29 | mpdd 43 |
. . . 4
Cgr
Cgr
Cgr Cgr
Cgr |
31 | | opeq1 4402 |
. . . . . . . 8
|
32 | 31 | breq2d 4665 |
. . . . . . 7
|
33 | 32 | anbi1d 741 |
. . . . . 6
|
34 | 31 | breq1d 4663 |
. . . . . . 7
Cgr
Cgr |
35 | 34 | anbi1d 741 |
. . . . . 6
Cgr Cgr
Cgr Cgr
|
36 | 33, 35 | 3anbi12d 1400 |
. . . . 5
Cgr
Cgr
Cgr Cgr Cgr
Cgr
Cgr Cgr |
37 | 36 | imbi1d 331 |
. . . 4
Cgr
Cgr
Cgr Cgr
Cgr
Cgr Cgr Cgr Cgr
Cgr |
38 | 30, 37 | syl5ibr 236 |
. . 3
Cgr
Cgr
Cgr Cgr
Cgr |
39 | | simp12 1092 |
. . . . . . 7
|
40 | | btwndiff 32134 |
. . . . . . 7
|
41 | 3, 39, 5, 40 | syl3anc 1326 |
. . . . . 6
|
42 | | simpl11 1136 |
. . . . . . . . . 10
|
43 | | simpl23 1141 |
. . . . . . . . . 10
|
44 | | simpl32 1143 |
. . . . . . . . . 10
|
45 | | simpl21 1139 |
. . . . . . . . . 10
|
46 | | simpr 477 |
. . . . . . . . . 10
|
47 | | axsegcon 25807 |
. . . . . . . . . 10
Cgr |
48 | 42, 43, 44, 45, 46, 47 | syl122anc 1335 |
. . . . . . . . 9
Cgr |
49 | | anass 681 |
. . . . . . . . . . . . 13
Cgr
Cgr
Cgr
Cgr Cgr
Cgr
Cgr
Cgr
Cgr Cgr |
50 | | anass 681 |
. . . . . . . . . . . . . 14
Cgr
Cgr Cgr Cgr Cgr
Cgr
Cgr
Cgr
Cgr Cgr |
51 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr
Cgr Cgr Cgr Cgr |
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Cgr
Cgr Cgr Cgr Cgr |
53 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr
Cgr Cgr Cgr Cgr |
54 | 53 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Cgr
Cgr Cgr Cgr Cgr |
55 | 52, 54 | jca 554 |
. . . . . . . . . . . . . . . . . . 19
Cgr
Cgr Cgr Cgr Cgr
|
56 | | simpr2l 1120 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr
Cgr Cgr Cgr Cgr Cgr |
57 | 56 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
Cgr
Cgr Cgr Cgr Cgr Cgr
|
58 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr Cgr Cgr Cgr Cgr |
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr
Cgr Cgr Cgr Cgr Cgr |
60 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr Cgr Cgr Cgr
|
61 | 20 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr Cgr Cgr Cgr
|
62 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr Cgr Cgr Cgr |
63 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr Cgr Cgr Cgr
|
64 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr Cgr Cgr Cgr |
65 | | cgrcom 32097 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr Cgr |
66 | 60, 61, 62, 63, 64, 65 | syl122anc 1335 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr |
67 | 59, 66 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
Cgr
Cgr Cgr Cgr Cgr Cgr |
68 | 57, 67 | jca 554 |
. . . . . . . . . . . . . . . . . . 19
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr |
69 | | simprr3 1111 |
. . . . . . . . . . . . . . . . . . 19
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr
|
70 | 55, 68, 69 | 3jca 1242 |
. . . . . . . . . . . . . . . . . 18
Cgr
Cgr Cgr Cgr Cgr
Cgr
Cgr
Cgr
Cgr |
71 | 70 | ex 450 |
. . . . . . . . . . . . . . . . 17
Cgr
Cgr Cgr Cgr Cgr
Cgr Cgr
Cgr
Cgr
|
72 | | simpl11 1136 |
. . . . . . . . . . . . . . . . . 18
|
73 | | simpl12 1137 |
. . . . . . . . . . . . . . . . . 18
|
74 | | simpl21 1139 |
. . . . . . . . . . . . . . . . . 18
|
75 | | simprl 794 |
. . . . . . . . . . . . . . . . . 18
|
76 | | simpl22 1140 |
. . . . . . . . . . . . . . . . . 18
|
77 | | simpl23 1141 |
. . . . . . . . . . . . . . . . . 18
|
78 | | simpl32 1143 |
. . . . . . . . . . . . . . . . . 18
|
79 | | simprr 796 |
. . . . . . . . . . . . . . . . . 18
|
80 | | simpl33 1144 |
. . . . . . . . . . . . . . . . . 18
|
81 | | brofs 32112 |
. . . . . . . . . . . . . . . . . 18
Cgr
Cgr
Cgr
Cgr |
82 | 72, 73, 74, 75, 76, 77, 78, 79, 80, 81 | syl333anc 1358 |
. . . . . . . . . . . . . . . . 17
Cgr
Cgr
Cgr
Cgr |
83 | 71, 82 | sylibrd 249 |
. . . . . . . . . . . . . . . 16
Cgr
Cgr Cgr Cgr Cgr |
84 | | 5segofs 32113 |
. . . . . . . . . . . . . . . . 17
Cgr |
85 | 72, 73, 74, 75, 76, 77, 78, 79, 80, 84 | syl333anc 1358 |
. . . . . . . . . . . . . . . 16
Cgr |
86 | 83, 85 | syland 498 |
. . . . . . . . . . . . . . 15
Cgr
Cgr Cgr Cgr Cgr Cgr |
87 | | simpr1l 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
Cgr
Cgr Cgr Cgr Cgr |
88 | 87 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Cgr
Cgr Cgr Cgr Cgr Cgr |
89 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Cgr
Cgr Cgr Cgr Cgr Cgr |
90 | 88, 89 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Cgr
Cgr Cgr Cgr Cgr Cgr |
91 | | simpr1r 1119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Cgr
Cgr Cgr Cgr Cgr |
92 | 91 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Cgr
Cgr Cgr Cgr Cgr Cgr |
93 | 53 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Cgr
Cgr Cgr Cgr Cgr Cgr |
94 | 90, 92, 93 | jca32 558 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Cgr
Cgr Cgr Cgr Cgr Cgr
|
95 | | simpl13 1138 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
96 | | btwnexch3 32127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
97 | 72, 73, 95, 74, 75, 96 | syl122anc 1335 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
98 | | simpl31 1142 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
99 | | btwnexch3 32127 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
100 | 72, 77, 98, 78, 79, 99 | syl122anc 1335 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
101 | 97, 100 | anim12d 586 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
102 | 94, 101 | syl5 34 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
Cgr Cgr Cgr Cgr Cgr |
103 | 102 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr Cgr Cgr Cgr Cgr
|
104 | | btwncom 32121 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
105 | 72, 74, 95, 75, 104 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
106 | | btwncom 32121 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
107 | 72, 78, 98, 79, 106 | syl13anc 1328 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
108 | 105, 107 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
109 | 108 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr Cgr Cgr Cgr Cgr
|
110 | 103, 109 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr Cgr Cgr Cgr Cgr
|
111 | 58 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr |
112 | 72, 78, 79, 74, 75, 65 | syl122anc 1335 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Cgr Cgr |
113 | | cgrcomlr 32105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
Cgr Cgr |
114 | 72, 74, 75, 78, 79, 113 | syl122anc 1335 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Cgr Cgr |
115 | 112, 114 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Cgr Cgr |
116 | 115 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr Cgr |
117 | 111, 116 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr |
118 | | simpr2r 1121 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Cgr
Cgr Cgr Cgr Cgr Cgr |
119 | 118 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr
|
120 | 72, 95, 74, 98, 78, 119 | cgrcomlrand 32108 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr
|
121 | 117, 120 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr Cgr
|
122 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr |
123 | | simpr3r 1123 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
Cgr Cgr Cgr Cgr Cgr |
124 | 123 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr
|
125 | 122, 124 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr Cgr
|
126 | 110, 121,
125 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr
Cgr Cgr Cgr Cgr Cgr
Cgr Cgr
Cgr Cgr |
127 | 126 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
Cgr
Cgr Cgr Cgr Cgr Cgr
Cgr Cgr Cgr Cgr |
128 | | brofs 32112 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr Cgr
Cgr Cgr |
129 | 72, 75, 74, 95, 76, 79, 78, 98, 80, 128 | syl333anc 1358 |
. . . . . . . . . . . . . . . . . . . 20
Cgr Cgr
Cgr Cgr |
130 | 127, 129 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . 19
Cgr
Cgr Cgr Cgr Cgr Cgr |
131 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr Cgr Cgr Cgr |
132 | 131 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr
Cgr Cgr Cgr Cgr Cgr |
133 | 132 | necomd 2849 |
. . . . . . . . . . . . . . . . . . . 20
Cgr
Cgr Cgr Cgr Cgr Cgr |
134 | 133 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
Cgr
Cgr Cgr Cgr Cgr Cgr |
135 | 130, 134 | jcad 555 |
. . . . . . . . . . . . . . . . . 18
Cgr
Cgr Cgr Cgr Cgr Cgr
|
136 | | 5segofs 32113 |
. . . . . . . . . . . . . . . . . . 19
Cgr |
137 | 72, 75, 74, 95, 76, 79, 78, 98, 80, 136 | syl333anc 1358 |
. . . . . . . . . . . . . . . . . 18
Cgr |
138 | 135, 137 | syld 47 |
. . . . . . . . . . . . . . . . 17
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr |
139 | 138 | expd 452 |
. . . . . . . . . . . . . . . 16
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr
|
140 | 139 | adantrd 484 |
. . . . . . . . . . . . . . 15
Cgr
Cgr Cgr Cgr Cgr Cgr Cgr
|
141 | 86, 140 | mpdd 43 |
. . . . . . . . . . . . . 14
Cgr
Cgr Cgr Cgr Cgr Cgr |
142 | 50, 141 | syl5bir 233 |
. . . . . . . . . . . . 13
Cgr
Cgr
Cgr
Cgr Cgr Cgr
|
143 | 49, 142 | syl5bir 233 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr
Cgr Cgr Cgr |
144 | 143 | expd 452 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr
Cgr Cgr Cgr
|
145 | 144 | anassrs 680 |
. . . . . . . . . 10
Cgr
Cgr
Cgr
Cgr Cgr Cgr
|
146 | 145 | rexlimdva 3031 |
. . . . . . . . 9
Cgr
Cgr
Cgr
Cgr Cgr Cgr
|
147 | 48, 146 | mpd 15 |
. . . . . . . 8
Cgr Cgr Cgr Cgr Cgr
|
148 | 147 | expd 452 |
. . . . . . 7
Cgr
Cgr
Cgr Cgr Cgr |
149 | 148 | rexlimdva 3031 |
. . . . . 6
Cgr
Cgr
Cgr Cgr Cgr |
150 | 41, 149 | mpd 15 |
. . . . 5
Cgr
Cgr
Cgr Cgr Cgr |
151 | 150 | expd 452 |
. . . 4
Cgr
Cgr
Cgr Cgr
Cgr |
152 | 151 | com3r 87 |
. . 3
Cgr
Cgr
Cgr Cgr
Cgr |
153 | 38, 152 | pm2.61ine 2877 |
. 2
Cgr
Cgr
Cgr Cgr
Cgr |
154 | 1, 153 | sylbid 230 |
1
Cgr |