Description: Cancellation law for subtraction ( pncan analog). (Contributed by NM, 16-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Hypotheses | grpsubadd.b | |
|
grpsubadd.p | |
||
grpsubadd.m | |
||
Assertion | grppncan | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | grpsubadd.b | |
|
2 | grpsubadd.p | |
|
3 | grpsubadd.m | |
|
4 | simp1 | |
|
5 | simp2 | |
|
6 | simp3 | |
|
7 | 1 2 3 | grpaddsubass | |
8 | 4 5 6 6 7 | syl13anc | |
9 | eqid | |
|
10 | 1 9 3 | grpsubid | |
11 | 10 | oveq2d | |
12 | 11 | 3adant2 | |
13 | 1 2 9 | grprid | |
14 | 13 | 3adant3 | |
15 | 8 12 14 | 3eqtrd | |