Step | Hyp | Ref
| Expression |
1 | | brcgr3 32153 |
. . . . . 6
Cgr3
Cgr
Cgr Cgr |
2 | | simp2 1062 |
. . . . . 6
Cgr
Cgr
Cgr
Cgr |
3 | 1, 2 | syl6bi 243 |
. . . . 5
Cgr3 Cgr |
4 | | simp1 1061 |
. . . . . 6
|
5 | | simp21 1094 |
. . . . . 6
|
6 | | simp22 1095 |
. . . . . 6
|
7 | | simp23 1096 |
. . . . . 6
|
8 | | simp31 1097 |
. . . . . 6
|
9 | | simp33 1099 |
. . . . . 6
|
10 | | cgrxfr 32162 |
. . . . . 6
Cgr
Cgr3
|
11 | 4, 5, 6, 7, 8, 9, 10 | syl132anc 1344 |
. . . . 5
Cgr
Cgr3 |
12 | 3, 11 | sylan2d 499 |
. . . 4
Cgr3
Cgr3 |
13 | 12 | imp 445 |
. . 3
Cgr3
Cgr3 |
14 | | simprrl 804 |
. . . . . . . . . . . . 13
Cgr3
Cgr3
|
15 | 14, 14 | jca 554 |
. . . . . . . . . . . 12
Cgr3
Cgr3
|
16 | | simpl1 1064 |
. . . . . . . . . . . . . . 15
|
17 | | simpl31 1142 |
. . . . . . . . . . . . . . 15
|
18 | | simpl33 1144 |
. . . . . . . . . . . . . . 15
|
19 | 16, 17, 18 | cgrrflxd 32095 |
. . . . . . . . . . . . . 14
Cgr |
20 | | simpr 477 |
. . . . . . . . . . . . . . 15
|
21 | 16, 20, 18 | cgrrflxd 32095 |
. . . . . . . . . . . . . 14
Cgr |
22 | 19, 21 | jca 554 |
. . . . . . . . . . . . 13
Cgr
Cgr |
23 | 22 | adantr 481 |
. . . . . . . . . . . 12
Cgr3
Cgr3
Cgr Cgr |
24 | | simpr 477 |
. . . . . . . . . . . . . 14
Cgr3
Cgr3
|
25 | | simpr 477 |
. . . . . . . . . . . . . 14
Cgr3
Cgr3
|
26 | | simpl2 1065 |
. . . . . . . . . . . . . . . 16
|
27 | | simpl3 1066 |
. . . . . . . . . . . . . . . 16
|
28 | 17, 20, 18 | 3jca 1242 |
. . . . . . . . . . . . . . . 16
|
29 | | cgr3tr4 32159 |
. . . . . . . . . . . . . . . 16
Cgr3
Cgr3
Cgr3
|
30 | 16, 26, 27, 28, 29 | syl13anc 1328 |
. . . . . . . . . . . . . . 15
Cgr3 Cgr3
Cgr3
|
31 | | cgr3com 32160 |
. . . . . . . . . . . . . . . . 17
Cgr3
Cgr3
|
32 | 16, 27, 17, 20, 18, 31 | syl113anc 1338 |
. . . . . . . . . . . . . . . 16
Cgr3
Cgr3
|
33 | | simpl32 1143 |
. . . . . . . . . . . . . . . . . 18
|
34 | | brcgr3 32153 |
. . . . . . . . . . . . . . . . . 18
Cgr3
Cgr
Cgr Cgr |
35 | 16, 17, 20, 18, 17, 33, 18, 34 | syl133anc 1349 |
. . . . . . . . . . . . . . . . 17
Cgr3
Cgr
Cgr Cgr |
36 | | simpr1 1067 |
. . . . . . . . . . . . . . . . . . 19
Cgr Cgr
Cgr
Cgr |
37 | | simpr3 1069 |
. . . . . . . . . . . . . . . . . . . 20
Cgr Cgr
Cgr
Cgr |
38 | 16, 20, 18, 33, 18, 37 | cgrcomlrand 32108 |
. . . . . . . . . . . . . . . . . . 19
Cgr Cgr
Cgr
Cgr |
39 | 36, 38 | jca 554 |
. . . . . . . . . . . . . . . . . 18
Cgr Cgr
Cgr
Cgr
Cgr |
40 | 39 | ex 450 |
. . . . . . . . . . . . . . . . 17
Cgr Cgr Cgr
Cgr Cgr |
41 | 35, 40 | sylbid 230 |
. . . . . . . . . . . . . . . 16
Cgr3 Cgr Cgr |
42 | 32, 41 | sylbid 230 |
. . . . . . . . . . . . . . 15
Cgr3 Cgr Cgr |
43 | 30, 42 | syld 47 |
. . . . . . . . . . . . . 14
Cgr3 Cgr3
Cgr
Cgr |
44 | 24, 25, 43 | syl2ani 688 |
. . . . . . . . . . . . 13
Cgr3
Cgr3
Cgr Cgr |
45 | 44 | imp 445 |
. . . . . . . . . . . 12
Cgr3
Cgr3
Cgr Cgr |
46 | 15, 23, 45 | 3jca 1242 |
. . . . . . . . . . 11
Cgr3
Cgr3
Cgr
Cgr Cgr Cgr |
47 | 46 | ex 450 |
. . . . . . . . . 10
Cgr3
Cgr3
Cgr
Cgr Cgr Cgr |
48 | | brifs 32150 |
. . . . . . . . . . . 12
Cgr
Cgr Cgr Cgr |
49 | | ifscgr 32151 |
. . . . . . . . . . . 12
Cgr |
50 | 48, 49 | sylbird 250 |
. . . . . . . . . . 11
Cgr
Cgr Cgr Cgr Cgr |
51 | 16, 17, 20, 18, 20, 17, 20, 18, 33, 50 | syl333anc 1358 |
. . . . . . . . . 10
Cgr
Cgr Cgr Cgr Cgr |
52 | 47, 51 | syld 47 |
. . . . . . . . 9
Cgr3
Cgr3
Cgr |
53 | | cgrid2 32110 |
. . . . . . . . . 10
Cgr |
54 | 16, 20, 20, 33, 53 | syl13anc 1328 |
. . . . . . . . 9
Cgr |
55 | 52, 54 | syld 47 |
. . . . . . . 8
Cgr3
Cgr3
|
56 | 55 | imp 445 |
. . . . . . 7
Cgr3
Cgr3
|
57 | 56, 14 | eqbrtrrd 4677 |
. . . . . 6
Cgr3
Cgr3
|
58 | 57 | expr 643 |
. . . . 5
Cgr3
Cgr3
|
59 | 58 | an32s 846 |
. . . 4
Cgr3
Cgr3
|
60 | 59 | rexlimdva 3031 |
. . 3
Cgr3
Cgr3
|
61 | 13, 60 | mpd 15 |
. 2
Cgr3 |
62 | 61 | ex 450 |
1
Cgr3
|