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

Metamath Proof Explorer

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 ) )