Metamath Proof Explorer

Theorem addsub

Description: Law for addition and subtraction. (Contributed by NM, 19-Aug-2001) (Proof shortened by Andrew Salmon, 22-Oct-2011)

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

Proof

Step Hyp Ref Expression
1 addcom 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
2 1 oveq1d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - C ) = ( ( B + A ) - C ) )
3 2 3adant3 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - C ) = ( ( B + A ) - C ) )
4 addsubass 
 |-  ( ( B e. CC /\ A e. CC /\ C e. CC ) -> ( ( B + A ) - C ) = ( B + ( A - C ) ) )
5 4 3com12 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B + A ) - C ) = ( B + ( A - C ) ) )
6 subcl 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A - C ) e. CC )
7 addcom 
 |-  ( ( B e. CC /\ ( A - C ) e. CC ) -> ( B + ( A - C ) ) = ( ( A - C ) + B ) )
8 6 7 sylan2 
 |-  ( ( B e. CC /\ ( A e. CC /\ C e. CC ) ) -> ( B + ( A - C ) ) = ( ( A - C ) + B ) )
9 8 3impb 
 |-  ( ( B e. CC /\ A e. CC /\ C e. CC ) -> ( B + ( A - C ) ) = ( ( A - C ) + B ) )
10 9 3com12 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B + ( A - C ) ) = ( ( A - C ) + B ) )
11 3 5 10 3eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - C ) = ( ( A - C ) + B ) )