Metamath Proof Explorer


Theorem subsub23i

Description: Swap subtrahend and result of subtraction. (Contributed by NM, 7-Oct-1999)

Ref Expression
Hypotheses negidi.1
|- A e. CC
pncan3i.2
|- B e. CC
subadd.3
|- C e. CC
Assertion subsub23i
|- ( ( A - B ) = C <-> ( A - C ) = B )

Proof

Step Hyp Ref Expression
1 negidi.1
 |-  A e. CC
2 pncan3i.2
 |-  B e. CC
3 subadd.3
 |-  C e. CC
4 subsub23
 |-  ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A - B ) = C <-> ( A - C ) = B ) )
5 1 2 3 4 mp3an
 |-  ( ( A - B ) = C <-> ( A - C ) = B )