Metamath Proof Explorer

Theorem rennncan2

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

Ref Expression
Assertion rennncan2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ C - ℝ B - ℝ C = A - ℝ B

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ
2 simp3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ
3 simp2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B ∈ ℝ
4 rersubcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B - ℝ C ∈ ℝ
5 3 2 4 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B - ℝ C ∈ ℝ
6 resubsub4 ⊢ A ∈ ℝ ∧ C ∈ ℝ ∧ B - ℝ C ∈ ℝ → A - ℝ C - ℝ B - ℝ C = A - ℝ C + B - ℝ C
7 1 2 5 6 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ C - ℝ B - ℝ C = A - ℝ C + B - ℝ C
8 repncan3 ⊢ C ∈ ℝ ∧ B ∈ ℝ → C + B - ℝ C = B
9 2 3 8 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C + B - ℝ C = B
10 9 oveq2d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ C + B - ℝ C = A - ℝ B
11 7 10 eqtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A - ℝ C - ℝ B - ℝ C = A - ℝ B