Theorem slt2addd

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

	Ref	Expression
Hypotheses	slt2addd.1	$$⊢\phi \to A\in \mathrm{No}$$
	slt2addd.2	$$⊢\phi \to B\in \mathrm{No}$$
	slt2addd.3	$$⊢\phi \to C\in \mathrm{No}$$
	slt2addd.4	$$⊢\phi \to D\in \mathrm{No}$$
	slt2addd.5	$$⊢\phi \to A{<}_{s}C$$
	slt2addd.6	$$⊢\phi \to B{<}_{s}D$$
Assertion	slt2addd	Could not format assertion : No typesetting found for |- ( ph -> ( A +s B )

Proof

Step	Hyp	Ref	Expression
1		slt2addd.1	$$⊢\phi \to A\in \mathrm{No}$$
2		slt2addd.2	$$⊢\phi \to B\in \mathrm{No}$$
3		slt2addd.3	$$⊢\phi \to C\in \mathrm{No}$$
4		slt2addd.4	$$⊢\phi \to D\in \mathrm{No}$$
5		slt2addd.5	$$⊢\phi \to A{<}_{s}C$$
6		slt2addd.6	$$⊢\phi \to B{<}_{s}D$$
7	1 2	addscld	Could not format ( ph -> ( A +s B ) e. No ) : No typesetting found for |- ( ph -> ( A +s B ) e. No ) with typecode |-
8	3 2	addscld	Could not format ( ph -> ( C +s B ) e. No ) : No typesetting found for |- ( ph -> ( C +s B ) e. No ) with typecode |-
9	3 4	addscld	Could not format ( ph -> ( C +s D ) e. No ) : No typesetting found for |- ( ph -> ( C +s D ) e. No ) with typecode |-
10	1 3 2	sltadd1d	Could not format ( ph -> ( A ( A +s B ) ( A ( A +s B )
11	5 10	mpbid	Could not format ( ph -> ( A +s B ) ( A +s B )
12	2 4 3	sltadd2d	Could not format ( ph -> ( B ( C +s B ) ( B ( C +s B )
13	6 12	mpbid	Could not format ( ph -> ( C +s B ) ( C +s B )
14	7 8 9 11 13	slttrd	Could not format ( ph -> ( A +s B ) ( A +s B )