Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 30-May-2012)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemd4.l | |
|
cdlemd4.j | |
||
cdlemd4.a | |
||
cdlemd4.h | |
||
cdlemd4.t | |
||
Assertion | cdlemd5 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemd4.l | |
|
2 | cdlemd4.j | |
|
3 | cdlemd4.a | |
|
4 | cdlemd4.h | |
|
5 | cdlemd4.t | |
|
6 | fveq2 | |
|
7 | fveq2 | |
|
8 | 6 7 | eqeq12d | |
9 | simpll1 | |
|
10 | simpl21 | |
|
11 | 10 | adantr | |
12 | simpl22 | |
|
13 | 12 | adantr | |
14 | simp23 | |
|
15 | 14 | ad2antrr | |
16 | simplr | |
|
17 | simpr | |
|
18 | 15 16 17 | 3jca | |
19 | simpll3 | |
|
20 | 1 2 3 4 5 | cdlemd4 | |
21 | 9 11 13 18 19 20 | syl131anc | |
22 | simpl3l | |
|
23 | 8 21 22 | pm2.61ne | |
24 | simpl1 | |
|
25 | simpl21 | |
|
26 | simpl22 | |
|
27 | simpl23 | |
|
28 | simpr | |
|
29 | 27 28 | jca | |
30 | simpl3 | |
|
31 | 1 2 3 4 5 | cdlemd2 | |
32 | 24 25 26 29 30 31 | syl131anc | |
33 | 23 32 | pm2.61dan | |