Description: Lemma for ablfac . (Contributed by Mario Carneiro, 27-Apr-2016) (Proof shortened by Mario Carneiro, 3-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ablfac.b | |
|
ablfac.c | |
||
ablfac.1 | |
||
ablfac.2 | |
||
ablfac.o | |
||
ablfac.a | |
||
ablfac.s | |
||
ablfac.w | |
||
ablfaclem2.f | |
||
ablfaclem2.q | |
||
ablfaclem2.l | |
||
ablfaclem2.g | |
||
Assertion | ablfaclem2 | |