Description: Obsolete version of psrass1lem as of 7-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | psrbag.d | |
|
psrbagconf1o.s | |
||
gsumbagdiagOLD.i | |
||
gsumbagdiagOLD.f | |
||
gsumbagdiagOLD.b | |
||
gsumbagdiagOLD.g | |
||
gsumbagdiagOLD.x | |
||
psrass1lemOLD.y | |
||
Assertion | psrass1lemOLD | |