Metamath Proof Explorer


Theorem subaddd

Description: Relationship between subtraction and addition. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses negidd.1 φ A
pncand.2 φ B
subaddd.3 φ C
Assertion subaddd φ A B = C B + C = A

Proof

Step Hyp Ref Expression
1 negidd.1 φ A
2 pncand.2 φ B
3 subaddd.3 φ C
4 subadd A B C A B = C B + C = A
5 1 2 3 4 syl3anc φ A B = C B + C = A