Theorem pnncan

Description: Cancellation law for mixed addition and subtraction. (Contributed by NM, 30-Jun-2005) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
2		simp2	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> B e. CC )
3	1 2	addcld	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + B ) e. CC )
4		simp3	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
5		subsub	|- ( ( ( A + B ) e. CC /\ A e. CC /\ C e. CC ) -> ( ( A + B ) - ( A - C ) ) = ( ( ( A + B ) - A ) + C ) )
6	3 1 4 5	syl3anc	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - ( A - C ) ) = ( ( ( A + B ) - A ) + C ) )
7		pncan2	|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - A ) = B )
8	7	3adant3	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - A ) = B )
9	8	oveq1d	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( ( A + B ) - A ) + C ) = ( B + C ) )
10	6 9	eqtrd	|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - ( A - C ) ) = ( B + C ) )