Step | Hyp | Ref
| Expression |
1 | | simpl1 1064 |
. . . 4
Cgr |
2 | | simpl3r 1117 |
. . . 4
Cgr |
3 | | simpl3l 1116 |
. . . 4
Cgr |
4 | | btwndiff 32134 |
. . . 4
|
5 | 1, 2, 3, 4 | syl3anc 1326 |
. . 3
Cgr
|
6 | | simpl1 1064 |
. . . . . . . . 9
|
7 | | simpr 477 |
. . . . . . . . 9
|
8 | | simpl3l 1116 |
. . . . . . . . 9
|
9 | | simpl21 1139 |
. . . . . . . . 9
|
10 | | simpl22 1140 |
. . . . . . . . 9
|
11 | | axsegcon 25807 |
. . . . . . . . 9
Cgr |
12 | 6, 7, 8, 9, 10, 11 | syl122anc 1335 |
. . . . . . . 8
Cgr |
13 | 12 | adantr 481 |
. . . . . . 7
Cgr
Cgr |
14 | | anass 681 |
. . . . . . . . . 10
|
15 | | simpl1 1064 |
. . . . . . . . . . . . . 14
|
16 | | simprl 794 |
. . . . . . . . . . . . . 14
|
17 | | simprr 796 |
. . . . . . . . . . . . . 14
|
18 | | simpl22 1140 |
. . . . . . . . . . . . . 14
|
19 | | simpl23 1141 |
. . . . . . . . . . . . . 14
|
20 | | axsegcon 25807 |
. . . . . . . . . . . . . 14
Cgr |
21 | 15, 16, 17, 18, 19, 20 | syl122anc 1335 |
. . . . . . . . . . . . 13
Cgr |
22 | 21 | adantr 481 |
. . . . . . . . . . . 12
Cgr
Cgr
Cgr |
23 | | anass 681 |
. . . . . . . . . . . . . . . 16
|
24 | | df-3an 1039 |
. . . . . . . . . . . . . . . . 17
|
25 | 24 | anbi2i 730 |
. . . . . . . . . . . . . . . 16
|
26 | 23, 25 | bitr4i 267 |
. . . . . . . . . . . . . . 15
|
27 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr |
28 | 27 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr
Cgr |
29 | 28 | necomd 2849 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr
Cgr
Cgr |
30 | | simpl1 1064 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
31 | | simpr1 1067 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
32 | | simpl3l 1116 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
33 | | simpr2 1068 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
34 | | simpr3 1069 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
35 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
Cgr |
36 | 35 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr
Cgr |
37 | | simprrl 804 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr
Cgr |
38 | 30, 31, 32, 33, 34, 36, 37 | btwnexchand 32133 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr
Cgr |
39 | | simpl21 1139 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
40 | | simpl22 1140 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
41 | | simpl23 1141 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
42 | 30, 31, 32, 33, 34, 36, 37 | btwnexch3and 32128 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr
Cgr |
43 | | simplll 798 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
Cgr |
44 | 43 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr
Cgr |
45 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
Cgr Cgr |
46 | 45 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr
Cgr Cgr |
47 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr
Cgr Cgr |
48 | 30, 32, 33, 34, 39, 40, 41, 42, 44, 46, 47 | cgrextendand 32116 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr
Cgr Cgr |
49 | 38, 48 | jca 554 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr
Cgr
Cgr Cgr |
50 | | simpl3r 1117 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
51 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
Cgr |
52 | 51 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr
Cgr |
53 | 30, 32, 50, 31, 52 | btwncomand 32122 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr
Cgr |
54 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
Cgr Cgr |
55 | 54 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr
Cgr Cgr |
56 | 30, 39, 41, 32, 50, 55 | cgrcomand 32098 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr
Cgr Cgr |
57 | 53, 56 | jca 554 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr
Cgr
Cgr Cgr
|
58 | 29, 49, 57 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . 20
Cgr
Cgr
Cgr
Cgr Cgr |
59 | 58 | ex 450 |
. . . . . . . . . . . . . . . . . . 19
Cgr Cgr
Cgr Cgr Cgr |
60 | | segconeq 32117 |
. . . . . . . . . . . . . . . . . . . 20
Cgr Cgr
|
61 | 30, 32, 39, 41, 31, 34, 50, 60 | syl133anc 1349 |
. . . . . . . . . . . . . . . . . . 19
Cgr Cgr
|
62 | 59, 61 | syld 47 |
. . . . . . . . . . . . . . . . . 18
Cgr Cgr
Cgr |
63 | 62 | imp 445 |
. . . . . . . . . . . . . . . . 17
Cgr
Cgr
Cgr |
64 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
65 | 64 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . . . . 22
|
66 | | opeq2 4403 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
67 | 66 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr Cgr |
68 | 65, 67 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr
Cgr |
69 | 68 | biimpa 501 |
. . . . . . . . . . . . . . . . . . . 20
Cgr
Cgr |
70 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
|
71 | | btwnexch3 32127 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
72 | 30, 31, 32, 33, 50, 71 | syl122anc 1335 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
73 | 35, 70, 72 | syl2ani 688 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr Cgr
Cgr |
74 | 73 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr
Cgr
|
75 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Cgr
Cgr
Cgr Cgr |
76 | 75 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
Cgr
Cgr Cgr |
77 | 30, 32, 33, 39, 40, 76 | cgrcomand 32098 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr
Cgr Cgr
|
78 | 54 | ad2antrl 764 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr
Cgr Cgr
|
79 | | simprrr 805 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr
Cgr
Cgr Cgr
|
80 | 30, 33, 50, 40, 41, 79 | cgrcomand 32098 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr
Cgr Cgr |
81 | | brcgr3 32153 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Cgr3
Cgr
Cgr Cgr |
82 | 30, 39, 40, 41, 32, 33, 50, 81 | syl133anc 1349 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Cgr3
Cgr
Cgr Cgr |
83 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
Cgr
Cgr
Cgr Cgr3 Cgr
Cgr
Cgr |
84 | 77, 78, 80, 83 | mpbir3and 1245 |
. . . . . . . . . . . . . . . . . . . . . 22
Cgr
Cgr
Cgr Cgr3 |
85 | 74, 84 | jca 554 |
. . . . . . . . . . . . . . . . . . . . 21
Cgr
Cgr
Cgr
Cgr3
|
86 | 85 | expr 643 |
. . . . . . . . . . . . . . . . . . . 20
Cgr
Cgr Cgr
Cgr3 |
87 | 69, 86 | syl5 34 |
. . . . . . . . . . . . . . . . . . 19
Cgr
Cgr Cgr
Cgr3
|
88 | 87 | expcomd 454 |
. . . . . . . . . . . . . . . . . 18
Cgr
Cgr Cgr
Cgr3 |
89 | 88 | impr 649 |
. . . . . . . . . . . . . . . . 17
Cgr
Cgr
Cgr
Cgr3 |
90 | 63, 89 | mpd 15 |
. . . . . . . . . . . . . . . 16
Cgr
Cgr
Cgr
Cgr3 |
91 | 90 | expr 643 |
. . . . . . . . . . . . . . 15
Cgr
Cgr Cgr
Cgr3 |
92 | 26, 91 | sylanb 489 |
. . . . . . . . . . . . . 14
Cgr
Cgr Cgr
Cgr3 |
93 | 92 | an32s 846 |
. . . . . . . . . . . . 13
Cgr
Cgr
Cgr
Cgr3 |
94 | 93 | rexlimdva 3031 |
. . . . . . . . . . . 12
Cgr
Cgr Cgr
Cgr3 |
95 | 22, 94 | mpd 15 |
. . . . . . . . . . 11
Cgr
Cgr
Cgr3
|
96 | 95 | expr 643 |
. . . . . . . . . 10
Cgr Cgr
Cgr3 |
97 | 14, 96 | sylanb 489 |
. . . . . . . . 9
Cgr
Cgr
Cgr3
|
98 | 97 | an32s 846 |
. . . . . . . 8
Cgr
Cgr
Cgr3
|
99 | 98 | reximdva 3017 |
. . . . . . 7
Cgr
Cgr
Cgr3 |
100 | 13, 99 | mpd 15 |
. . . . . 6
Cgr
Cgr3 |
101 | 100 | expr 643 |
. . . . 5
Cgr
Cgr3 |
102 | 101 | an32s 846 |
. . . 4
Cgr
Cgr3 |
103 | 102 | rexlimdva 3031 |
. . 3
Cgr
Cgr3 |
104 | 5, 103 | mpd 15 |
. 2
Cgr
Cgr3 |
105 | 104 | ex 450 |
1
Cgr
Cgr3
|