This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem subaddeqd

Description: Transfer two terms of a subtraction to an addition in an equality. (Contributed by Thierry Arnoux, 2-Feb-2020)

Ref Expression
Hypotheses subaddeqd.a 
|- ( ph -> A e. CC )
subaddeqd.b 
|- ( ph -> B e. CC )
subaddeqd.c 
|- ( ph -> C e. CC )
subaddeqd.d 
|- ( ph -> D e. CC )
subaddeqd.1 
|- ( ph -> ( A + B ) = ( C + D ) )
Assertion subaddeqd 
|- ( ph -> ( A - D ) = ( C - B ) )

Proof

Step Hyp Ref Expression
1 subaddeqd.a 
 |-  ( ph -> A e. CC )
2 subaddeqd.b 
 |-  ( ph -> B e. CC )
3 subaddeqd.c 
 |-  ( ph -> C e. CC )
4 subaddeqd.d 
 |-  ( ph -> D e. CC )
5 subaddeqd.1 
 |-  ( ph -> ( A + B ) = ( C + D ) )
6 5 oveq1d 
 |-  ( ph -> ( ( A + B ) - ( D + B ) ) = ( ( C + D ) - ( D + B ) ) )
7 3 4 addcomd 
 |-  ( ph -> ( C + D ) = ( D + C ) )
8 7 oveq1d 
 |-  ( ph -> ( ( C + D ) - ( D + B ) ) = ( ( D + C ) - ( D + B ) ) )
9 6 8 eqtrd 
 |-  ( ph -> ( ( A + B ) - ( D + B ) ) = ( ( D + C ) - ( D + B ) ) )
10 1 4 2 pnpcan2d 
 |-  ( ph -> ( ( A + B ) - ( D + B ) ) = ( A - D ) )
11 4 3 2 pnpcand 
 |-  ( ph -> ( ( D + C ) - ( D + B ) ) = ( C - B ) )
12 9 10 11 3eqtr3d 
 |-  ( ph -> ( A - D ) = ( C - B ) )