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 |
|
subrngsubg |
Could not format ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) ) : No typesetting found for |- ( I e. ( SubRng ` R ) -> I e. ( SubGrp ` R ) ) with typecode |- |
6 |
|
eqid |
|
7 |
6
|
subg0cl |
|
8 |
4 5 7
|
3syl |
|