Metamath Proof Explorer

Theorem reppncan

Description: Cancellation law for mixed addition and real subtraction. Compare ppncan . (Contributed by SN, 3-Sep-2023)

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

Proof

Step Hyp Ref Expression
1 repnpcan ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B - ℝ A + C = B - ℝ C
2 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
3 2 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B ∈ ℝ
4 readdcl ⊢ A ∈ ℝ ∧ C ∈ ℝ → A + C ∈ ℝ
5 4 3adant2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + C ∈ ℝ
6 rersubcl ⊢ B ∈ ℝ ∧ C ∈ ℝ → B - ℝ C ∈ ℝ
7 6 3adant1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → B - ℝ C ∈ ℝ
8 3 5 7 resubaddd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B - ℝ A + C = B - ℝ C ↔ A + C + B - ℝ C = A + B
9 1 8 mpbid ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + C + B - ℝ C = A + B