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

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 ⊢ ( 𝜑 → ( ( 𝐴 −ℝ 𝐵 ) = 𝐶 ↔ ( 𝐵 + 𝐶 ) = 𝐴 ) )