Metamath Proof Explorer


Theorem subaddsd

Description: Relationship between addition and subtraction for surreals. (Contributed by Scott Fenton, 5-Feb-2025)

Ref Expression
Hypotheses subaddsd.1 ( 𝜑𝐴 No )
subaddsd.2 ( 𝜑𝐵 No )
subaddsd.3 ( 𝜑𝐶 No )
Assertion subaddsd ( 𝜑 → ( ( 𝐴 -s 𝐵 ) = 𝐶 ↔ ( 𝐵 +s 𝐶 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 subaddsd.1 ( 𝜑𝐴 No )
2 subaddsd.2 ( 𝜑𝐵 No )
3 subaddsd.3 ( 𝜑𝐶 No )
4 subadds ( ( 𝐴 No 𝐵 No 𝐶 No ) → ( ( 𝐴 -s 𝐵 ) = 𝐶 ↔ ( 𝐵 +s 𝐶 ) = 𝐴 ) )
5 1 2 3 4 syl3anc ( 𝜑 → ( ( 𝐴 -s 𝐵 ) = 𝐶 ↔ ( 𝐵 +s 𝐶 ) = 𝐴 ) )