Theorem repnpcan

Description: Cancellation law for addition and real subtraction. Compare pnpcan . (Contributed by Steven Nguyen, 19-May-2023)

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

Proof

Step	Hyp	Ref	Expression
1		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
2		resubsub4	⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) −ℝ 𝐶 ) = ( ( 𝐴 + 𝐵 ) −ℝ ( 𝐴 + 𝐶 ) ) )
3	1 2	stoic4a	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) −ℝ 𝐶 ) = ( ( 𝐴 + 𝐵 ) −ℝ ( 𝐴 + 𝐶 ) ) )
4		repncan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) = 𝐵 )
5	4	3adant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) = 𝐵 )
6	5	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) −ℝ 𝐴 ) −ℝ 𝐶 ) = ( 𝐵 −ℝ 𝐶 ) )
7	3 6	eqtr3d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) −ℝ ( 𝐴 + 𝐶 ) ) = ( 𝐵 −ℝ 𝐶 ) )