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 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴𝐵 ) = 𝐶 ↔ ( 𝐶 + 𝐵 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 subadd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴𝐵 ) = 𝐶 ↔ ( 𝐵 + 𝐶 ) = 𝐴 ) )
2 simp2 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐵 ∈ ℂ )
3 simp3 ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → 𝐶 ∈ ℂ )
4 2 3 addcomd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐵 + 𝐶 ) = ( 𝐶 + 𝐵 ) )
5 4 eqeq1d ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐵 + 𝐶 ) = 𝐴 ↔ ( 𝐶 + 𝐵 ) = 𝐴 ) )
6 1 5 bitrd ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( ( 𝐴𝐵 ) = 𝐶 ↔ ( 𝐶 + 𝐵 ) = 𝐴 ) )