Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 23-Feb-2013)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cdleme31fv2.f | |
|
Assertion | cdleme31fv2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdleme31fv2.f | |
|
2 | breq1 | |
|
3 | 2 | notbid | |
4 | 3 | anbi2d | |
5 | 4 | notbid | |
6 | 5 | biimparc | |
7 | 6 | adantll | |
8 | 7 | iffalsed | |
9 | simpr | |
|
10 | 8 9 | eqtrd | |
11 | simpl | |
|
12 | 1 10 11 11 | fvmptd2 | |