Theorem slt2addd

Description: Adding both sides of two surreal less-than relations. (Contributed by Scott Fenton, 15-Apr-2025)

	Ref	Expression
Hypotheses	slt2addd.1	|- ( ph -> A e. No )
	slt2addd.2	|- ( ph -> B e. No )
	slt2addd.3	|- ( ph -> C e. No )
	slt2addd.4	|- ( ph -> D e. No )
	slt2addd.5	|- ( ph -> A
	slt2addd.6	|- ( ph -> B
Assertion	slt2addd	|- ( ph -> ( A +s B )

Proof

Step	Hyp	Ref	Expression
1		slt2addd.1	|- ( ph -> A e. No )
2		slt2addd.2	|- ( ph -> B e. No )
3		slt2addd.3	|- ( ph -> C e. No )
4		slt2addd.4	|- ( ph -> D e. No )
5		slt2addd.5	|- ( ph -> A
6		slt2addd.6	|- ( ph -> B
7	1 2	addscld	|- ( ph -> ( A +s B ) e. No )
8	3 2	addscld	|- ( ph -> ( C +s B ) e. No )
9	3 4	addscld	|- ( ph -> ( C +s D ) e. No )
10	1 3 2	sltadd1d	|- ( ph -> ( A ( A +s B )
11	5 10	mpbid	|- ( ph -> ( A +s B )
12	2 4 3	sltadd2d	|- ( ph -> ( B ( C +s B )
13	6 12	mpbid	|- ( ph -> ( C +s B )
14	7 8 9 11 13	slttrd	|- ( ph -> ( A +s B )