Description: Lemma 2 for cramer . (Contributed by AV, 21-Feb-2019) (Revised by AV, 1-Mar-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cramer.a | |
|
cramer.b | |
||
cramer.v | |
||
cramer.d | |
||
cramer.x | |
||
cramer.q | |
||
Assertion | cramerlem2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cramer.a | |
|
2 | cramer.b | |
|
3 | cramer.v | |
|
4 | cramer.d | |
|
5 | cramer.x | |
|
6 | cramer.q | |
|
7 | simpll1 | |
|
8 | simpll2 | |
|
9 | simpll3 | |
|
10 | simplr | |
|
11 | simpr | |
|
12 | 1 2 3 4 5 6 | cramerlem1 | |
13 | 7 8 9 10 11 12 | syl113anc | |
14 | 13 | ex | |
15 | 14 | ralrimiva | |