This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B - ℝ A + C = B - ℝ C

Proof

Step Hyp Ref Expression
1 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
2 resubsub4 ⊢ A + B ∈ ℝ ∧ A ∈ ℝ ∧ C ∈ ℝ → A + B - ℝ A - ℝ C = A + B - ℝ A + C
3 1 2 stoic4a ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B - ℝ A - ℝ C = A + B - ℝ A + C
4 repncan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B - ℝ A = B
5 4 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B - ℝ A = B
6 5 oveq1d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B - ℝ A - ℝ C = B - ℝ C
7 3 6 eqtr3d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B - ℝ A + C = B - ℝ C