This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → ( 𝐴 = ( 𝐶 − 𝐵 ) ↔ 𝐵 = ( 𝐶 − 𝐴 ) ) )