Description: Cancellation law for surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nncansd.1 | ||
nncansd.2 | |||
Assertion | nncansd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nncansd.1 | ||
2 | nncansd.2 | ||
3 | 1 1 2 | subsubs2d | |
4 | pncan3s | ||
5 | 1 2 4 | syl2anc | |
6 | 3 5 | eqtrd |