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

Metamath Proof Explorer

Theorem npcan

Description: Cancellation law for subtraction. (Contributed by NM, 10-May-2004) (Revised by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Assertion	npcan	$⊢ (A \in ℂ \land B \in ℂ) \to A - B + B = A$

Step	Hyp	Ref	Expression
1		subcl	$⊢ (A \in ℂ \land B \in ℂ) \to A - B \in ℂ$
2		simpr	$⊢ (A \in ℂ \land B \in ℂ) \to B \in ℂ$
3	1 2	addcomd	$⊢ (A \in ℂ \land B \in ℂ) \to A - B + B = B + A - B$
4		pncan3	$⊢ (B \in ℂ \land A \in ℂ) \to B + A - B = A$
5	4	ancoms	$⊢ (A \in ℂ \land B \in ℂ) \to B + A - B = A$
6	3 5	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to A - B + B = A$