Description: Lemma for tsmsxp . (Contributed by Mario Carneiro, 21-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tsmsxp.b | |
|
tsmsxp.g | |
||
tsmsxp.2 | |
||
tsmsxp.a | |
||
tsmsxp.c | |
||
tsmsxp.f | |
||
tsmsxp.h | |
||
tsmsxp.1 | |
||
tsmsxp.j | |
||
tsmsxp.z | |
||
tsmsxp.p | |
||
tsmsxp.m | |
||
tsmsxp.l | |
||
tsmsxp.3 | |
||
tsmsxp.k | |
||
tsmsxp.4 | |
||
tsmsxp.n | |
||
tsmsxp.s | |
||
tsmsxp.x | |
||
tsmsxp.5 | |
||
tsmsxp.6 | |
||
Assertion | tsmsxplem2 | |