Description: Law for double surreal subtraction. (Contributed by Scott Fenton, 16-Apr-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | subsubs4d.1 | ||
subsubs4d.2 | |||
subsubs4d.3 | |||
Assertion | subsubs2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | subsubs4d.1 | ||
2 | subsubs4d.2 | ||
3 | subsubs4d.3 | ||
4 | 2 3 | subscld | |
5 | 1 4 | subsvald | |
6 | 2 3 | negsubsdi2d | |
7 | 6 | oveq2d | |
8 | 5 7 | eqtrd |