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