Metamath Proof Explorer


Theorem resubaddd

Description: Relationship between subtraction and addition. Based on subaddd . (Contributed by Steven Nguyen, 8-Jan-2023)

Ref Expression
Hypotheses resubaddd.1 ( 𝜑𝐴 ∈ ℝ )
resubaddd.2 ( 𝜑𝐵 ∈ ℝ )
resubaddd.3 ( 𝜑𝐶 ∈ ℝ )
Assertion resubaddd ( 𝜑 → ( ( 𝐴 𝐵 ) = 𝐶 ↔ ( 𝐵 + 𝐶 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 resubaddd.1 ( 𝜑𝐴 ∈ ℝ )
2 resubaddd.2 ( 𝜑𝐵 ∈ ℝ )
3 resubaddd.3 ( 𝜑𝐶 ∈ ℝ )
4 resubadd ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 𝐵 ) = 𝐶 ↔ ( 𝐵 + 𝐶 ) = 𝐴 ) )
5 1 2 3 4 syl3anc ( 𝜑 → ( ( 𝐴 𝐵 ) = 𝐶 ↔ ( 𝐵 + 𝐶 ) = 𝐴 ) )