Metamath Proof Explorer


Theorem subexsub

Description: A subtraction law: Exchanging the subtrahend and the result of the subtraction. (Contributed by BJ, 6-Jun-2019)

Ref Expression
Hypotheses addlsub.a
|- ( ph -> A e. CC )
addlsub.b
|- ( ph -> B e. CC )
addlsub.c
|- ( ph -> C e. CC )
Assertion subexsub
|- ( ph -> ( A = ( C - B ) <-> B = ( C - A ) ) )

Proof

Step Hyp Ref Expression
1 addlsub.a
 |-  ( ph -> A e. CC )
2 addlsub.b
 |-  ( ph -> B e. CC )
3 addlsub.c
 |-  ( ph -> C e. CC )
4 1 2 3 addlsub
 |-  ( ph -> ( ( A + B ) = C <-> A = ( C - B ) ) )
5 1 2 3 addrsub
 |-  ( ph -> ( ( A + B ) = C <-> B = ( C - A ) ) )
6 4 5 bitr3d
 |-  ( ph -> ( A = ( C - B ) <-> B = ( C - A ) ) )