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