Metamath Proof Explorer


Theorem int-eqmvtd

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

Ref Expression
Hypotheses int-eqmvtd.1 ( 𝜑𝐶 ∈ ℝ )
int-eqmvtd.2 ( 𝜑𝐷 ∈ ℝ )
int-eqmvtd.3 ( 𝜑𝐴 = 𝐵 )
int-eqmvtd.4 ( 𝜑𝐴 = ( 𝐶 + 𝐷 ) )
Assertion int-eqmvtd ( 𝜑𝐶 = ( 𝐵𝐷 ) )

Proof

Step Hyp Ref Expression
1 int-eqmvtd.1 ( 𝜑𝐶 ∈ ℝ )
2 int-eqmvtd.2 ( 𝜑𝐷 ∈ ℝ )
3 int-eqmvtd.3 ( 𝜑𝐴 = 𝐵 )
4 int-eqmvtd.4 ( 𝜑𝐴 = ( 𝐶 + 𝐷 ) )
5 3 4 eqtr3d ( 𝜑𝐵 = ( 𝐶 + 𝐷 ) )
6 5 oveq1d ( 𝜑 → ( 𝐵𝐷 ) = ( ( 𝐶 + 𝐷 ) − 𝐷 ) )
7 1 recnd ( 𝜑𝐶 ∈ ℂ )
8 2 recnd ( 𝜑𝐷 ∈ ℂ )
9 7 8 pncand ( 𝜑 → ( ( 𝐶 + 𝐷 ) − 𝐷 ) = 𝐶 )
10 6 9 eqtrd ( 𝜑 → ( 𝐵𝐷 ) = 𝐶 )
11 10 eqcomd ( 𝜑𝐶 = ( 𝐵𝐷 ) )