reppncan

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

		Ref	Expression
	Assertion	reppncan	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A + C + (B -_{ℝ} C) = A + B$

Step	Hyp	Ref	Expression
1		repnpcan	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to (A + B) -_{ℝ} (A + C) = B -_{ℝ} C$
2		readdcl	$⊢ (A \in ℝ \land B \in ℝ) \to A + B \in ℝ$
3	2	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A + B \in ℝ$
4		readdcl	$⊢ (A \in ℝ \land C \in ℝ) \to A + C \in ℝ$
5	4	3adant2	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A + C \in ℝ$
6		rersubcl	$⊢ (B \in ℝ \land C \in ℝ) \to B -_{ℝ} C \in ℝ$
7	6	3adant1	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to B -_{ℝ} C \in ℝ$
8	3 5 7	resubaddd	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to ((A + B) -_{ℝ} (A + C) = B -_{ℝ} C \leftrightarrow A + C + (B -_{ℝ} C) = A + B)$
9	1 8	mpbid	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to A + C + (B -_{ℝ} C) = A + B$

Metamath Proof Explorer