Theorem pncan2

Description: Cancellation law for subtraction. (Contributed by NM, 17-Apr-2005)

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

Proof

Step	Hyp	Ref	Expression
1		addcom	|- ( ( B e. CC /\ A e. CC ) -> ( B + A ) = ( A + B ) )
2	1	oveq1d	|- ( ( B e. CC /\ A e. CC ) -> ( ( B + A ) - A ) = ( ( A + B ) - A ) )
3		pncan	|- ( ( B e. CC /\ A e. CC ) -> ( ( B + A ) - A ) = B )
4	2 3	eqtr3d	|- ( ( B e. CC /\ A e. CC ) -> ( ( A + B ) - A ) = B )
5	4	ancoms	|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - A ) = B )