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	$$⊢\phi \to A\in ℂ$$
	addlsub.b	$$⊢\phi \to B\in ℂ$$
	addlsub.c	$$⊢\phi \to C\in ℂ$$
Assertion	addrsub	$$⊢\phi \to \left(A+B=C\leftrightarrow B=C-A\right)$$

Proof

Step	Hyp	Ref	Expression
1		addlsub.a	$$⊢\phi \to A\in ℂ$$
2		addlsub.b	$$⊢\phi \to B\in ℂ$$
3		addlsub.c	$$⊢\phi \to C\in ℂ$$
4	1 2	addcomd	$$⊢\phi \to A+B=B+A$$
5	4	eqeq1d	$$⊢\phi \to \left(A+B=C\leftrightarrow B+A=C\right)$$
6	2 1 3	addlsub	$$⊢\phi \to \left(B+A=C\leftrightarrow B=C-A\right)$$
7	5 6	bitrd	$$⊢\phi \to \left(A+B=C\leftrightarrow B=C-A\right)$$