Step |
Hyp |
Ref |
Expression |
1 |
|
rng2idlsubrng.r |
|
2 |
|
rng2idlsubrng.i |
|
3 |
|
rng2idlsubrng.u |
|
4 |
1 2 3
|
rng2idlsubrng |
Could not format ( ph -> I e. ( SubRng ` R ) ) : No typesetting found for |- ( ph -> I e. ( SubRng ` R ) ) with typecode |- |
5 |
|
subrngringnsg |
Could not format ( I e. ( SubRng ` R ) -> I e. ( NrmSGrp ` R ) ) : No typesetting found for |- ( I e. ( SubRng ` R ) -> I e. ( NrmSGrp ` R ) ) with typecode |- |
6 |
4 5
|
syl |
|