Metamath Proof Explorer

Theorem subsub23

Description: Swap subtrahend and result of subtraction. (Contributed by NM, 14-Dec-2007)

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

Proof

Step Hyp Ref Expression
1 addcom 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B + C ) = ( C + B ) )
2 1 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( B + C ) = ( C + B ) )
3 2 eqeq1d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( B + C ) = A <-> ( C + B ) = A ) )
4 subadd 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( B + C ) = A ) )
5 subadd 
 |-  ( ( A e. CC /\ C e. CC /\ B e. CC ) -> ( ( A - C ) = B <-> ( C + B ) = A ) )
6 5 3com23 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - C ) = B <-> ( C + B ) = A ) )
7 3 4 6 3bitr4d 
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( A - C ) = B ) )