Step |
Hyp |
Ref |
Expression |
1 |
|
qsidom.1 |
|
2 |
1
|
qsidomlem1 |
Could not format ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ Q e. IDomn ) -> I e. ( PrmIdeal ` R ) ) : No typesetting found for |- ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ Q e. IDomn ) -> I e. ( PrmIdeal ` R ) ) with typecode |- |
3 |
1
|
qsidomlem2 |
Could not format ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn ) : No typesetting found for |- ( ( R e. CRing /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn ) with typecode |- |
4 |
3
|
adantlr |
Could not format ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn ) : No typesetting found for |- ( ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) /\ I e. ( PrmIdeal ` R ) ) -> Q e. IDomn ) with typecode |- |
5 |
2 4
|
impbida |
Could not format ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> ( Q e. IDomn <-> I e. ( PrmIdeal ` R ) ) ) : No typesetting found for |- ( ( R e. CRing /\ I e. ( LIdeal ` R ) ) -> ( Q e. IDomn <-> I e. ( PrmIdeal ` R ) ) ) with typecode |- |