Step |
Hyp |
Ref |
Expression |
1 |
|
simpll |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> A e. CC ) |
2 |
|
simplr |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> B e. CC ) |
3 |
|
simprl |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> C e. CC ) |
4 |
|
addsub |
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) - C ) = ( ( A - C ) + B ) ) |
5 |
1 2 3 4
|
syl3anc |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) - C ) = ( ( A - C ) + B ) ) |
6 |
5
|
oveq1d |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A + B ) - C ) - D ) = ( ( ( A - C ) + B ) - D ) ) |
7 |
1 2
|
addcld |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A + B ) e. CC ) |
8 |
|
simprr |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> D e. CC ) |
9 |
|
subsub4 |
|- ( ( ( A + B ) e. CC /\ C e. CC /\ D e. CC ) -> ( ( ( A + B ) - C ) - D ) = ( ( A + B ) - ( C + D ) ) ) |
10 |
7 3 8 9
|
syl3anc |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A + B ) - C ) - D ) = ( ( A + B ) - ( C + D ) ) ) |
11 |
|
subcl |
|- ( ( A e. CC /\ C e. CC ) -> ( A - C ) e. CC ) |
12 |
11
|
ad2ant2r |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( A - C ) e. CC ) |
13 |
|
addsubass |
|- ( ( ( A - C ) e. CC /\ B e. CC /\ D e. CC ) -> ( ( ( A - C ) + B ) - D ) = ( ( A - C ) + ( B - D ) ) ) |
14 |
12 2 8 13
|
syl3anc |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( ( A - C ) + B ) - D ) = ( ( A - C ) + ( B - D ) ) ) |
15 |
6 10 14
|
3eqtr3d |
|- ( ( ( A e. CC /\ B e. CC ) /\ ( C e. CC /\ D e. CC ) ) -> ( ( A + B ) - ( C + D ) ) = ( ( A - C ) + ( B - D ) ) ) |