Metamath Proof Explorer

Theorem cnapbmcpd

Description: ((a+b)-c)+d = ((a+d)+b)-c holds for complex numbers a,b,c,d. (Contributed by Alexander van der Vekens, 23-Mar-2018)

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

Proof

Step Hyp Ref Expression
1 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
2 1 adantr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A + B ) e. CC )
3 simpr 
 |-  ( ( C e. CC /\ D e. CC ) -> D e. CC )
4 3 adantl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> D e. CC )
5 simpl 
 |-  ( ( C e. CC /\ D e. CC ) -> C e. CC )
6 5 adantl 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> C e. CC )
7 2 4 6 addsubd 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A + B ) + D ) - C ) = ( ( ( A + B ) - C ) + D ) )
8 simpl 
 |-  ( ( A e. CC /\ B e. CC ) -> A e. CC )
9 8 adantr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> A e. CC )
10 simpr 
 |-  ( ( A e. CC /\ B e. CC ) -> B e. CC )
11 10 adantr 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> B e. CC )
12 9 11 4 add32d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) + D ) = ( ( A + D ) + B ) )
13 12 oveq1d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A + B ) + D ) - C ) = ( ( ( A + D ) + B ) - C ) )
14 7 13 eqtr3d 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A + B ) - C ) + D ) = ( ( ( A + D ) + B ) - C ) )