Theorem rennncan2

Description: Cancellation law for real subtraction. Compare nnncan2 . (Contributed by Steven Nguyen, 14-Jan-2023)

	Ref	Expression
Assertion	rennncan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐶 ) −ℝ ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐴 −ℝ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐴 ∈ ℝ )
2		simp3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ )
3		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ )
4		rersubcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
5	3 2 4	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 −ℝ 𝐶 ) ∈ ℝ )
6		resubsub4	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ ( 𝐵 −ℝ 𝐶 ) ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐶 ) −ℝ ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐴 −ℝ ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) ) )
7	1 2 5 6	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐶 ) −ℝ ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐴 −ℝ ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) ) )
8		repncan3	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐵 )
9	2 3 8	syl2anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) = 𝐵 )
10	9	oveq2d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 −ℝ ( 𝐶 + ( 𝐵 −ℝ 𝐶 ) ) ) = ( 𝐴 −ℝ 𝐵 ) )
11	7 10	eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 −ℝ 𝐶 ) −ℝ ( 𝐵 −ℝ 𝐶 ) ) = ( 𝐴 −ℝ 𝐵 ) )