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 ( 𝜑𝐴 ∈ ℂ )
addlsub.b ( 𝜑𝐵 ∈ ℂ )
addlsub.c ( 𝜑𝐶 ∈ ℂ )
Assertion subexsub ( 𝜑 → ( 𝐴 = ( 𝐶𝐵 ) ↔ 𝐵 = ( 𝐶𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 addlsub.a ( 𝜑𝐴 ∈ ℂ )
2 addlsub.b ( 𝜑𝐵 ∈ ℂ )
3 addlsub.c ( 𝜑𝐶 ∈ ℂ )
4 1 2 3 addlsub ( 𝜑 → ( ( 𝐴 + 𝐵 ) = 𝐶𝐴 = ( 𝐶𝐵 ) ) )
5 1 2 3 addrsub ( 𝜑 → ( ( 𝐴 + 𝐵 ) = 𝐶𝐵 = ( 𝐶𝐴 ) ) )
6 4 5 bitr3d ( 𝜑 → ( 𝐴 = ( 𝐶𝐵 ) ↔ 𝐵 = ( 𝐶𝐴 ) ) )