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	$$⊢\phi \to A\in ℂ$$
	addlsub.b	$$⊢\phi \to B\in ℂ$$
	addlsub.c	$$⊢\phi \to C\in ℂ$$
Assertion	subexsub	$$⊢\phi \to \left(A=C-B\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 3	addlsub	$$⊢\phi \to \left(A+B=C\leftrightarrow A=C-B\right)$$
5	1 2 3	addrsub	$$⊢\phi \to \left(A+B=C\leftrightarrow B=C-A\right)$$
6	4 5	bitr3d	$$⊢\phi \to \left(A=C-B\leftrightarrow B=C-A\right)$$