Description: Lemma for mdetuni . (Contributed by SO, 15-Jul-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | mdetuni.a | |
|
mdetuni.b | |
||
mdetuni.k | |
||
mdetuni.0g | |
||
mdetuni.1r | |
||
mdetuni.pg | |
||
mdetuni.tg | |
||
mdetuni.n | |
||
mdetuni.r | |
||
mdetuni.ff | |
||
mdetuni.al | |
||
mdetuni.li | |
||
mdetuni.sc | |
||
Assertion | mdetunilem7 | |