Metamath Proof Explorer

Theorem pncans

Description: Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion pncans ⊢ A ∈ No ∧ B ∈ No → A + s B - s B = A

Proof

Step Hyp Ref Expression
1 addscom ⊢ A ∈ No ∧ B ∈ No → A + s B = B + s A
2 1 eqcomd ⊢ A ∈ No ∧ B ∈ No → B + s A = A + s B
3 addscl ⊢ A ∈ No ∧ B ∈ No → A + s B ∈ No
4 simpr ⊢ A ∈ No ∧ B ∈ No → B ∈ No
5 simpl ⊢ A ∈ No ∧ B ∈ No → A ∈ No
6 3 4 5 subaddsd ⊢ A ∈ No ∧ B ∈ No → A + s B - s B = A ↔ B + s A = A + s B
7 2 6 mpbird ⊢ A ∈ No ∧ B ∈ No → A + s B - s B = A