Description: Implication 2 for lindslininds . (Contributed by AV, 26-Apr-2019) (Revised by AV, 30-Jul-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lindslinind.r | |
|
lindslinind.b | |
||
lindslinind.0 | |
||
lindslinind.z | |
||
Assertion | lindslinindsimp2 | |