Theorem lt2addsd

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

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

Proof

Step	Hyp	Ref	Expression
1		lt2addsd.1	|- ( ph -> A e. No )
2		lt2addsd.2	|- ( ph -> B e. No )
3		lt2addsd.3	|- ( ph -> C e. No )
4		lt2addsd.4	|- ( ph -> D e. No )
5		lt2addsd.5	|- ( ph -> A
6		lt2addsd.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	ltadds1d	|- ( ph -> ( A ( A +s B )
11	5 10	mpbid	|- ( ph -> ( A +s B )
12	2 4 3	ltadds2d	|- ( ph -> ( B ( C +s B )
13	6 12	mpbid	|- ( ph -> ( C +s B )
14	7 8 9 11 13	ltstrd	|- ( ph -> ( A +s B )