Theorem int-eqmvtd

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

	Ref	Expression
Hypotheses	int-eqmvtd.1	|- ( ph -> C e. RR )
	int-eqmvtd.2	|- ( ph -> D e. RR )
	int-eqmvtd.3	|- ( ph -> A = B )
	int-eqmvtd.4	|- ( ph -> A = ( C + D ) )
Assertion	int-eqmvtd	|- ( ph -> C = ( B - D ) )

Proof

Step	Hyp	Ref	Expression
1		int-eqmvtd.1	|- ( ph -> C e. RR )
2		int-eqmvtd.2	|- ( ph -> D e. RR )
3		int-eqmvtd.3	|- ( ph -> A = B )
4		int-eqmvtd.4	|- ( ph -> A = ( C + D ) )
5	3 4	eqtr3d	|- ( ph -> B = ( C + D ) )
6	5	oveq1d	|- ( ph -> ( B - D ) = ( ( C + D ) - D ) )
7	1	recnd	|- ( ph -> C e. CC )
8	2	recnd	|- ( ph -> D e. CC )
9	7 8	pncand	|- ( ph -> ( ( C + D ) - D ) = C )
10	6 9	eqtrd	|- ( ph -> ( B - D ) = C )
11	10	eqcomd	|- ( ph -> C = ( B - D ) )