Metamath Proof Explorer


Theorem resubaddd

Description: Relationship between subtraction and addition. Based on subaddd . (Contributed by Steven Nguyen, 8-Jan-2023)

Ref Expression
Hypotheses resubaddd.1 φ A
resubaddd.2 φ B
resubaddd.3 φ C
Assertion resubaddd φ A - B = C B + C = A

Proof

Step Hyp Ref Expression
1 resubaddd.1 φ A
2 resubaddd.2 φ B
3 resubaddd.3 φ C
4 resubadd A B C A - B = C B + C = A
5 1 2 3 4 syl3anc φ A - B = C B + C = A