Theorem subexsub

Description: A subtraction law: Exchanging the subtrahend and the result of the subtraction. (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	subexsub	|- ( ph -> ( A = ( C - B ) <-> B = ( C - A ) ) )

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	1 2 3	addlsub	|- ( ph -> ( ( A + B ) = C <-> A = ( C - B ) ) )
5	1 2 3	addrsub	|- ( ph -> ( ( A + B ) = C <-> B = ( C - A ) ) )
6	4 5	bitr3d	|- ( ph -> ( A = ( C - B ) <-> B = ( C - A ) ) )