Description: Lemma for archiabl . (Contributed by Thierry Arnoux, 1-May-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | archiabllem.b | |
|
archiabllem.0 | |
||
archiabllem.e | |
||
archiabllem.t | |
||
archiabllem.m | |
||
archiabllem.g | |
||
archiabllem.a | |
||
archiabllem2.1 | |
||
archiabllem2.2 | |
||
archiabllem2.3 | |
||
archiabllem2b.4 | |
||
archiabllem2b.5 | |
||
Assertion | archiabllem2b | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | archiabllem.b | |
|
2 | archiabllem.0 | |
|
3 | archiabllem.e | |
|
4 | archiabllem.t | |
|
5 | archiabllem.m | |
|
6 | archiabllem.g | |
|
7 | archiabllem.a | |
|
8 | archiabllem2.1 | |
|
9 | archiabllem2.2 | |
|
10 | archiabllem2.3 | |
|
11 | archiabllem2b.4 | |
|
12 | archiabllem2b.5 | |
|
13 | 1 2 3 4 5 6 7 8 9 10 11 12 | archiabllem2c | |
14 | 1 2 3 4 5 6 7 8 9 10 12 11 | archiabllem2c | |
15 | isogrp | |
|
16 | 15 | simprbi | |
17 | omndtos | |
|
18 | 6 16 17 | 3syl | |
19 | ogrpgrp | |
|
20 | 6 19 | syl | |
21 | 1 8 | grpcl | |
22 | 20 11 12 21 | syl3anc | |
23 | 1 8 | grpcl | |
24 | 20 12 11 23 | syl3anc | |
25 | 1 4 | tlt3 | |
26 | 18 22 24 25 | syl3anc | |
27 | 13 14 26 | ecase23d | |