Metamath Proof Explorer


Theorem subadd2

Description: Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion subadd2 ABCAB=CC+B=A

Proof

Step Hyp Ref Expression
1 subadd ABCAB=CB+C=A
2 simp2 ABCB
3 simp3 ABCC
4 2 3 addcomd ABCB+C=C+B
5 4 eqeq1d ABCB+C=AC+B=A
6 1 5 bitrd ABCAB=CC+B=A