Description: Lemma for pgpfac . (Contributed by Mario Carneiro, 27-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pgpfac.b | |
|
pgpfac.c | |
||
pgpfac.g | |
||
pgpfac.p | |
||
pgpfac.f | |
||
pgpfac.u | |
||
pgpfac.a | |
||
Assertion | pgpfaclem3 | |