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	$$⊢\phi \to A\in ℂ$$
	addlsub.b	$$⊢\phi \to B\in ℂ$$
	addlsub.c	$$⊢\phi \to C\in ℂ$$
Assertion	addlsub	$$⊢\phi \to \left(A+B=C\leftrightarrow A=C-B\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		oveq1	$$⊢A+B=C\to A+B-B=C-B$$
5	1 2	pncand	$$⊢\phi \to A+B-B=A$$
6		eqtr2	$$⊢\left(A+B-B=C-B\wedge A+B-B=A\right)\to C-B=A$$
7	6	eqcomd	$$⊢\left(A+B-B=C-B\wedge A+B-B=A\right)\to A=C-B$$
8	7	a1i	$$⊢\phi \to \left(\left(A+B-B=C-B\wedge A+B-B=A\right)\to A=C-B\right)$$
9	5 8	mpan2d	$$⊢\phi \to \left(A+B-B=C-B\to A=C-B\right)$$
10	4 9	syl5	$$⊢\phi \to \left(A+B=C\to A=C-B\right)$$
11		oveq1	$$⊢A=C-B\to A+B=C-B+B$$
12	3 2	npcand	$$⊢\phi \to C-B+B=C$$
13		eqtr	$$⊢\left(A+B=C-B+B\wedge C-B+B=C\right)\to A+B=C$$
14	13	a1i	$$⊢\phi \to \left(\left(A+B=C-B+B\wedge C-B+B=C\right)\to A+B=C\right)$$
15	12 14	mpan2d	$$⊢\phi \to \left(A+B=C-B+B\to A+B=C\right)$$
16	11 15	syl5	$$⊢\phi \to \left(A=C-B\to A+B=C\right)$$
17	10 16	impbid	$$⊢\phi \to \left(A+B=C\leftrightarrow A=C-B\right)$$