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	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	addlsub.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	addlsub.c	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion	subexsub	⊢ ( 𝜑 → ( 𝐴 = ( 𝐶 − 𝐵 ) ↔ 𝐵 = ( 𝐶 − 𝐴 ) ) )

Proof

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