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

Metamath Proof Explorer

Theorem addlsub

Description: Left-subtraction: Subtraction of the left 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 addlsub ⊢ φ → A + B = C ↔ A = C − B

Proof

Step Hyp Ref Expression
1 addlsub.a ⊢ φ → A ∈ ℂ
2 addlsub.b ⊢ φ → B ∈ ℂ
3 addlsub.c ⊢ φ → C ∈ ℂ
4 oveq1 ⊢ A + B = C → A + B - B = C − B
5 1 2 pncand ⊢ φ → A + B - B = A
6 eqtr2 ⊢ A + B - B = C − B ∧ A + B - B = A → C − B = A
7 6 eqcomd ⊢ A + B - B = C − B ∧ A + B - B = A → A = C − B
8 7 a1i ⊢ φ → A + B - B = C − B ∧ A + B - B = A → A = C − B
9 5 8 mpan2d ⊢ φ → A + B - B = C − B → A = C − B
10 4 9 syl5 ⊢ φ → A + B = C → A = C − B
11 oveq1 ⊢ A = C − B → A + B = C - B + B
12 3 2 npcand ⊢ φ → C - B + B = C
13 eqtr ⊢ A + B = C - B + B ∧ C - B + B = C → A + B = C
14 13 a1i ⊢ φ → A + B = C - B + B ∧ C - B + B = C → A + B = C
15 12 14 mpan2d ⊢ φ → A + B = C - B + B → A + B = C
16 11 15 syl5 ⊢ φ → A = C − B → A + B = C
17 10 16 impbid ⊢ φ → A + B = C ↔ A = C − B