Metamath Proof Explorer

Theorem addsub12

Description: Commutative/associative law for addition and subtraction. (Contributed by NM, 8-Feb-2005)

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

Proof

Step Hyp Ref Expression
1 subadd23 
 |-  ( ( A e. CC /\ C e. CC /\ B e. CC ) -> ( ( A - C ) + B ) = ( A + ( B - C ) ) )
2 subcl 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A - C ) e. CC )
3 addcom 
 |-  ( ( ( A - C ) e. CC /\ B e. CC ) -> ( ( A - C ) + B ) = ( B + ( A - C ) ) )
4 2 3 stoic3 
 |-  ( ( A e. CC /\ C e. CC /\ B e. CC ) -> ( ( A - C ) + B ) = ( B + ( A - C ) ) )
5 1 4 eqtr3d 
 |-  ( ( A e. CC /\ C e. CC /\ B e. CC ) -> ( A + ( B - C ) ) = ( B + ( A - C ) ) )
6 5 3com23 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( A + ( B - C ) ) = ( B + ( A - C ) ) )