Description: Lemma for pcohtpy . (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 24-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pcohtpy.4 | |
|
pcohtpy.5 | |
||
pcohtpy.6 | |
||
pcohtpylem.7 | |
||
pcohtpylem.8 | |
||
pcohtpylem.9 | |
||
Assertion | pcohtpylem | |