Description: TODO FIX COMMENT v_1 <_ r \/ g(s) p. 116 3rd line. (Contributed by NM, 3-Apr-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemef46g.b | |
|
cdlemef46g.l | |
||
cdlemef46g.j | |
||
cdlemef46g.m | |
||
cdlemef46g.a | |
||
cdlemef46g.h | |
||
cdlemef46g.u | |
||
cdlemef46g.d | |
||
cdlemefs46g.e | |
||
cdlemef46g.f | |
||
cdlemef46.v | |
||
cdlemef46.n | |
||
cdlemefs46.o | |
||
cdlemef46.g | |
||
cdlemeg46.y | |
||
cdlemeg46.x | |
||
Assertion | cdlemeg46vrg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemef46g.b | |
|
2 | cdlemef46g.l | |
|
3 | cdlemef46g.j | |
|
4 | cdlemef46g.m | |
|
5 | cdlemef46g.a | |
|
6 | cdlemef46g.h | |
|
7 | cdlemef46g.u | |
|
8 | cdlemef46g.d | |
|
9 | cdlemefs46g.e | |
|
10 | cdlemef46g.f | |
|
11 | cdlemef46.v | |
|
12 | cdlemef46.n | |
|
13 | cdlemefs46.o | |
|
14 | cdlemef46.g | |
|
15 | cdlemeg46.y | |
|
16 | cdlemeg46.x | |
|
17 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 | cdlemeg46v1v2 | |
18 | 17 15 | eqtrdi | |
19 | simp11l | |
|
20 | 19 | hllatd | |
21 | simp22l | |
|
22 | simp1 | |
|
23 | simp23 | |
|
24 | simp21 | |
|
25 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 | cdlemeg46fvaw | |
26 | 25 | simpld | |
27 | 22 23 24 26 | syl3anc | |
28 | 1 3 5 | hlatjcl | |
29 | 19 21 27 28 | syl3anc | |
30 | simp11r | |
|
31 | 1 6 | lhpbase | |
32 | 30 31 | syl | |
33 | 1 2 4 | latmle1 | |
34 | 20 29 32 33 | syl3anc | |
35 | 18 34 | eqbrtrd | |