Theorem int-eqmvtd

Description: EquMoveTerm generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

	Ref	Expression
Hypotheses	int-eqmvtd.1	$$⊢\phi \to C\in ℝ$$
	int-eqmvtd.2	$$⊢\phi \to D\in ℝ$$
	int-eqmvtd.3	$$⊢\phi \to A=B$$
	int-eqmvtd.4	$$⊢\phi \to A=C+D$$
Assertion	int-eqmvtd	$$⊢\phi \to C=B-D$$

Proof

Step	Hyp	Ref	Expression
1		int-eqmvtd.1	$$⊢\phi \to C\in ℝ$$
2		int-eqmvtd.2	$$⊢\phi \to D\in ℝ$$
3		int-eqmvtd.3	$$⊢\phi \to A=B$$
4		int-eqmvtd.4	$$⊢\phi \to A=C+D$$
5	3 4	eqtr3d	$$⊢\phi \to B=C+D$$
6	5	oveq1d	$$⊢\phi \to B-D=C+D-D$$
7	1	recnd	$$⊢\phi \to C\in ℂ$$
8	2	recnd	$$⊢\phi \to D\in ℂ$$
9	7 8	pncand	$$⊢\phi \to C+D-D=C$$
10	6 9	eqtrd	$$⊢\phi \to B-D=C$$
11	10	eqcomd	$$⊢\phi \to C=B-D$$