Description: Lemma for dvferm . (Contributed by Mario Carneiro, 24-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dvferm.a | |
|
dvferm.b | |
||
dvferm.u | |
||
dvferm.s | |
||
dvferm.d | |
||
dvferm2.r | |
||
dvferm2.z | |
||
dvferm2.t | |
||
dvferm2.l | |
||
dvferm2.x | |
||
Assertion | dvferm2lem | |