Metamath Proof Explorer


Theorem subcan2

Description: Cancellation law for subtraction. (Contributed by NM, 8-Feb-2005)

Ref Expression
Assertion subcan2 A B C A C = B C A = B

Proof

Step Hyp Ref Expression
1 simp1 A B C A
2 simp3 A B C C
3 subcl B C B C
4 3 3adant1 A B C B C
5 subadd2 A C B C A C = B C B - C + C = A
6 1 2 4 5 syl3anc A B C A C = B C B - C + C = A
7 npcan B C B - C + C = B
8 7 3adant1 A B C B - C + C = B
9 8 eqeq1d A B C B - C + C = A B = A
10 eqcom B = A A = B
11 9 10 bitrdi A B C B - C + C = A A = B
12 6 11 bitrd A B C A C = B C A = B