Metamath Proof Explorer

Theorem subadd2

Description: Relationship between subtraction and addition. (Contributed by Scott Fenton, 5-Jul-2013) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion subadd2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B=C↔C+B=A

Proof

Step Hyp Ref Expression
1 subadd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B=C↔B+C=A
2 simp2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B∈ℂ
3 simp3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→C∈ℂ
4 2 3 addcomd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+C=C+B
5 4 eqeq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B+C=A↔C+B=A
6 1 5 bitrd ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A−B=C↔C+B=A