Description: Lemma for imasdsf1o . (Contributed by Mario Carneiro, 21-Aug-2015) (Proof shortened by AV, 6-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | imasdsf1o.u | |
|
imasdsf1o.v | |
||
imasdsf1o.f | |
||
imasdsf1o.r | |
||
imasdsf1o.e | |
||
imasdsf1o.d | |
||
imasdsf1o.m | |
||
imasdsf1o.x | |
||
imasdsf1o.y | |
||
imasdsf1o.w | |
||
imasdsf1o.s | |
||
imasdsf1o.t | |
||
Assertion | imasdsf1olem | |