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 ) )