Step |
Hyp |
Ref |
Expression |
1 |
|
subrgmcl.p |
|
2 |
|
subrgsubrng |
Could not format ( A e. ( SubRing ` R ) -> A e. ( SubRng ` R ) ) : No typesetting found for |- ( A e. ( SubRing ` R ) -> A e. ( SubRng ` R ) ) with typecode |- |
3 |
1
|
subrngmcl |
Could not format ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A ) : No typesetting found for |- ( ( A e. ( SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A ) with typecode |- |
4 |
2 3
|
syl3an1 |
|