Theorem addrsub

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

	Ref	Expression
Hypotheses	addlsub.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	addlsub.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	addlsub.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion	addrsub	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) = 𝐶 ↔ 𝐵 = ( 𝐶 − 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		addlsub.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		addlsub.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		addlsub.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
4	1 2	addcomd	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
5	4	eqeq1d	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) = 𝐶 ↔ ( 𝐵 + 𝐴 ) = 𝐶 ) )
6	2 1 3	addlsub	⊢ ( 𝜑 → ( ( 𝐵 + 𝐴 ) = 𝐶 ↔ 𝐵 = ( 𝐶 − 𝐴 ) ) )
7	5 6	bitrd	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) = 𝐶 ↔ 𝐵 = ( 𝐶 − 𝐴 ) ) )