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

Metamath Proof Explorer

Theorem addrsub

Description: Right-subtraction: Subtraction of the right summand from the result of an addition. (Contributed by BJ, 6-Jun-2019)

Ref Expression
Hypotheses addlsub.a ⊢ φ → A ∈ ℂ
addlsub.b ⊢ φ → B ∈ ℂ
addlsub.c ⊢ φ → C ∈ ℂ
Assertion addrsub ⊢ φ → A + B = C ↔ B = C − A

Proof

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