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 ⊢ φ → A ∈ ℂ
addlsub.b ⊢ φ → B ∈ ℂ
addlsub.c ⊢ φ → C ∈ ℂ
Assertion subexsub ⊢ φ → A = C − B ↔ B = C − A

Proof

Step Hyp Ref Expression
1 addlsub.a ⊢ φ → A ∈ ℂ
2 addlsub.b ⊢ φ → B ∈ ℂ
3 addlsub.c ⊢ φ → C ∈ ℂ
4 1 2 3 addlsub ⊢ φ → A + B = C ↔ A = C − B
5 1 2 3 addrsub ⊢ φ → A + B = C ↔ B = C − A
6 4 5 bitr3d ⊢ φ → A = C − B ↔ B = C − A