Description: Lemma for resubdrg and friends. (Contributed by Mario Carneiro, 4-Dec-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cnsubglem.1 | |
|
cnsubglem.2 | |
||
cnsubglem.3 | |
||
cnsubrglem.4 | |
||
cnsubrglem.5 | |
||
Assertion | cnsubrglem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnsubglem.1 | |
|
2 | cnsubglem.2 | |
|
3 | cnsubglem.3 | |
|
4 | cnsubrglem.4 | |
|
5 | cnsubrglem.5 | |
|
6 | 1 2 3 4 | cnsubglem | |
7 | 5 | rgen2 | |
8 | cnring | |
|
9 | cnfldbas | |
|
10 | cnfld1 | |
|
11 | cnfldmul | |
|
12 | 9 10 11 | issubrg2 | |
13 | 8 12 | ax-mp | |
14 | 6 4 7 13 | mpbir3an | |