Metamath Proof Explorer


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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) − ( 𝐴 + 𝐶 ) ) = ( 𝐵 𝐶 ) )