Theorem pncan

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

	Ref	Expression
Assertion	pncan	|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - B ) = A )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( A e. CC /\ B e. CC ) -> B e. CC )
2		simpl	|- ( ( A e. CC /\ B e. CC ) -> A e. CC )
3	1 2	addcomd	|- ( ( A e. CC /\ B e. CC ) -> ( B + A ) = ( A + B ) )
4		addcl	|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
5		subadd	|- ( ( ( A + B ) e. CC /\ B e. CC /\ A e. CC ) -> ( ( ( A + B ) - B ) = A <-> ( B + A ) = ( A + B ) ) )
6	4 1 2 5	syl3anc	|- ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) - B ) = A <-> ( B + A ) = ( A + B ) ) )
7	3 6	mpbird	|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - B ) = A )