Theorem addlsub

Description: Left-subtraction: Subtraction of the left summand from the result of an addition. (Contributed by BJ, 6-Jun-2019)

	Ref	Expression
Hypotheses	addlsub.a	|- ( ph -> A e. CC )
	addlsub.b	|- ( ph -> B e. CC )
	addlsub.c	|- ( ph -> C e. CC )
Assertion	addlsub	|- ( ph -> ( ( A + B ) = C <-> A = ( C - B ) ) )

Proof

Step	Hyp	Ref	Expression
1		addlsub.a	|- ( ph -> A e. CC )
2		addlsub.b	|- ( ph -> B e. CC )
3		addlsub.c	|- ( ph -> C e. CC )
4		oveq1	|- ( ( A + B ) = C -> ( ( A + B ) - B ) = ( C - B ) )
5	1 2	pncand	|- ( ph -> ( ( A + B ) - B ) = A )
6		eqtr2	|- ( ( ( ( A + B ) - B ) = ( C - B ) /\ ( ( A + B ) - B ) = A ) -> ( C - B ) = A )
7	6	eqcomd	|- ( ( ( ( A + B ) - B ) = ( C - B ) /\ ( ( A + B ) - B ) = A ) -> A = ( C - B ) )
8	7	a1i	|- ( ph -> ( ( ( ( A + B ) - B ) = ( C - B ) /\ ( ( A + B ) - B ) = A ) -> A = ( C - B ) ) )
9	5 8	mpan2d	|- ( ph -> ( ( ( A + B ) - B ) = ( C - B ) -> A = ( C - B ) ) )
10	4 9	syl5	|- ( ph -> ( ( A + B ) = C -> A = ( C - B ) ) )
11		oveq1	|- ( A = ( C - B ) -> ( A + B ) = ( ( C - B ) + B ) )
12	3 2	npcand	|- ( ph -> ( ( C - B ) + B ) = C )
13		eqtr	|- ( ( ( A + B ) = ( ( C - B ) + B ) /\ ( ( C - B ) + B ) = C ) -> ( A + B ) = C )
14	13	a1i	|- ( ph -> ( ( ( A + B ) = ( ( C - B ) + B ) /\ ( ( C - B ) + B ) = C ) -> ( A + B ) = C ) )
15	12 14	mpan2d	|- ( ph -> ( ( A + B ) = ( ( C - B ) + B ) -> ( A + B ) = C ) )
16	11 15	syl5	|- ( ph -> ( A = ( C - B ) -> ( A + B ) = C ) )
17	10 16	impbid	|- ( ph -> ( ( A + B ) = C <-> A = ( C - B ) ) )