Metamath Proof Explorer

Theorem subsub2

Description: Law for double subtraction. (Contributed by NM, 30-Jun-2005) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 subcl 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
2 1 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B - C ) e. CC )
3 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> A e. CC )
4 simp3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> C e. CC )
5 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> B e. CC )
6 subcl 
 |-  ( ( C e. CC /\ B e. CC ) -> ( C - B ) e. CC )
7 4 5 6 syl2anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( C - B ) e. CC )
8 2 3 7 add12d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B - C ) + ( A + ( C - B ) ) ) = ( A + ( ( B - C ) + ( C - B ) ) ) )
9 npncan2 
 |-  ( ( B e. CC /\ C e. CC ) -> ( ( B - C ) + ( C - B ) ) = 0 )
10 9 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B - C ) + ( C - B ) ) = 0 )
11 10 oveq2d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( ( B - C ) + ( C - B ) ) ) = ( A + 0 ) )
12 3 addid1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + 0 ) = A )
13 8 11 12 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B - C ) + ( A + ( C - B ) ) ) = A )
14 3 7 addcld 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( C - B ) ) e. CC )
15 subadd 
 |-  ( ( A e. CC /\ ( B - C ) e. CC /\ ( A + ( C - B ) ) e. CC ) -> ( ( A - ( B - C ) ) = ( A + ( C - B ) ) <-> ( ( B - C ) + ( A + ( C - B ) ) ) = A ) )
16 3 2 14 15 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - ( B - C ) ) = ( A + ( C - B ) ) <-> ( ( B - C ) + ( A + ( C - B ) ) ) = A ) )
17 13 16 mpbird 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A - ( B - C ) ) = ( A + ( C - B ) ) )