Step | Hyp | Ref
| Expression |
1 | | opeq1 4402 |
. . . . 5
|
2 | 1 | breq2d 4665 |
. . . 4
|
3 | 2 | anbi1d 741 |
. . 3
|
4 | | opeq1 4402 |
. . . . 5
|
5 | 4 | breq1d 4663 |
. . . 4
Cgr
Cgr |
6 | 5 | anbi1d 741 |
. . 3
Cgr Cgr
Cgr Cgr |
7 | | opeq1 4402 |
. . . . 5
|
8 | 7 | breq1d 4663 |
. . . 4
Cgr Cgr |
9 | 8 | anbi1d 741 |
. . 3
Cgr Cgr Cgr Cgr |
10 | 3, 6, 9 | 3anbi123d 1399 |
. 2
Cgr Cgr
Cgr Cgr Cgr Cgr
Cgr Cgr |
11 | | breq1 4656 |
. . . 4
|
12 | 11 | anbi1d 741 |
. . 3
|
13 | | opeq2 4403 |
. . . . 5
|
14 | 13 | breq1d 4663 |
. . . 4
Cgr
Cgr |
15 | | opeq1 4402 |
. . . . 5
|
16 | 15 | breq1d 4663 |
. . . 4
Cgr
Cgr |
17 | 14, 16 | anbi12d 747 |
. . 3
Cgr Cgr
Cgr Cgr |
18 | | opeq1 4402 |
. . . . 5
|
19 | 18 | breq1d 4663 |
. . . 4
Cgr Cgr |
20 | 19 | anbi2d 740 |
. . 3
Cgr Cgr Cgr Cgr |
21 | 12, 17, 20 | 3anbi123d 1399 |
. 2
Cgr Cgr
Cgr Cgr Cgr Cgr
Cgr Cgr |
22 | | opeq2 4403 |
. . . . 5
|
23 | 22 | breq2d 4665 |
. . . 4
|
24 | 23 | anbi1d 741 |
. . 3
|
25 | | opeq2 4403 |
. . . . 5
|
26 | 25 | breq1d 4663 |
. . . 4
Cgr
Cgr |
27 | 26 | anbi2d 740 |
. . 3
Cgr Cgr
Cgr Cgr |
28 | 24, 27 | 3anbi12d 1400 |
. 2
Cgr Cgr
Cgr Cgr Cgr Cgr
Cgr
Cgr |
29 | | opeq2 4403 |
. . . . 5
|
30 | 29 | breq1d 4663 |
. . . 4
Cgr Cgr |
31 | | opeq2 4403 |
. . . . 5
|
32 | 31 | breq1d 4663 |
. . . 4
Cgr Cgr |
33 | 30, 32 | anbi12d 747 |
. . 3
Cgr Cgr Cgr Cgr |
34 | 33 | 3anbi3d 1405 |
. 2
Cgr Cgr
Cgr
Cgr
Cgr Cgr
Cgr
Cgr |
35 | | opeq1 4402 |
. . . . 5
|
36 | 35 | breq2d 4665 |
. . . 4
|
37 | 36 | anbi2d 740 |
. . 3
|
38 | | opeq1 4402 |
. . . . 5
|
39 | 38 | breq2d 4665 |
. . . 4
Cgr
Cgr
|
40 | 39 | anbi1d 741 |
. . 3
Cgr Cgr Cgr Cgr |
41 | | opeq1 4402 |
. . . . 5
|
42 | 41 | breq2d 4665 |
. . . 4
Cgr Cgr |
43 | 42 | anbi1d 741 |
. . 3
Cgr Cgr Cgr Cgr |
44 | 37, 40, 43 | 3anbi123d 1399 |
. 2
Cgr Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr |
45 | | breq1 4656 |
. . . 4
|
46 | 45 | anbi2d 740 |
. . 3
|
47 | | opeq2 4403 |
. . . . 5
|
48 | 47 | breq2d 4665 |
. . . 4
Cgr
Cgr |
49 | | opeq1 4402 |
. . . . 5
|
50 | 49 | breq2d 4665 |
. . . 4
Cgr
Cgr
|
51 | 48, 50 | anbi12d 747 |
. . 3
Cgr Cgr Cgr Cgr |
52 | | opeq1 4402 |
. . . . 5
|
53 | 52 | breq2d 4665 |
. . . 4
Cgr Cgr |
54 | 53 | anbi2d 740 |
. . 3
Cgr Cgr Cgr Cgr
|
55 | 46, 51, 54 | 3anbi123d 1399 |
. 2
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr
Cgr Cgr |
56 | | opeq2 4403 |
. . . . 5
|
57 | 56 | breq2d 4665 |
. . . 4
|
58 | 57 | anbi2d 740 |
. . 3
|
59 | | opeq2 4403 |
. . . . 5
|
60 | 59 | breq2d 4665 |
. . . 4
Cgr
Cgr |
61 | 60 | anbi2d 740 |
. . 3
Cgr Cgr
Cgr Cgr
|
62 | 58, 61 | 3anbi12d 1400 |
. 2
Cgr
Cgr
Cgr Cgr Cgr
Cgr
Cgr Cgr |
63 | | opeq2 4403 |
. . . . 5
|
64 | 63 | breq2d 4665 |
. . . 4
Cgr
Cgr |
65 | | opeq2 4403 |
. . . . 5
|
66 | 65 | breq2d 4665 |
. . . 4
Cgr
Cgr |
67 | 64, 66 | anbi12d 747 |
. . 3
Cgr Cgr
Cgr Cgr
|
68 | 67 | 3anbi3d 1405 |
. 2
Cgr
Cgr
Cgr Cgr Cgr
Cgr
Cgr Cgr |
69 | | fveq2 6191 |
. 2
|
70 | | df-ofs 32090 |
. 2
Cgr Cgr
Cgr Cgr |
71 | 10, 21, 28, 34, 44, 55, 62, 68, 69, 70 | br8 31646 |
1
Cgr
Cgr
Cgr Cgr |