Description: Part of proof of Lemma G of Crawley p. 116, fifth line of third paragraph on p. 117: "and hence fg = gf." (Contributed by NM, 3-Jun-2013)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemg44.h | |
|
cdlemg44.t | |
||
cdlemg44.r | |
||
Assertion | cdlemg44 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemg44.h | |
|
2 | cdlemg44.t | |
|
3 | cdlemg44.r | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 4 5 1 | lhpexnle | |
7 | 6 | 3ad2ant1 | |
8 | simp11 | |
|
9 | simp12l | |
|
10 | simp12r | |
|
11 | 1 2 | ltrnco | |
12 | 8 9 10 11 | syl3anc | |
13 | 1 2 | ltrnco | |
14 | 8 10 9 13 | syl3anc | |
15 | 3simpc | |
|
16 | simp13 | |
|
17 | 1 2 3 4 5 | cdlemg44b | |
18 | 8 9 10 15 16 17 | syl131anc | |
19 | simp12 | |
|
20 | simp2 | |
|
21 | 4 5 1 2 | ltrncoval | |
22 | 8 19 20 21 | syl3anc | |
23 | 4 5 1 2 | ltrncoval | |
24 | 8 10 9 20 23 | syl121anc | |
25 | 18 22 24 | 3eqtr4d | |
26 | 4 5 1 2 | cdlemd | |
27 | 8 12 14 15 25 26 | syl311anc | |
28 | 27 | rexlimdv3a | |
29 | 7 28 | mpd | |