sbthlem2 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem sbthlem2 4454

Description: Lemma for sbth 4463.

**Hypotheses**
Ref	Expression
sbthlem.1
sbthlem.2	$/\$

**Assertion**
Ref	Expression
sbthlem2

**Proof of Theorem sbthlem2**
Step	Hyp	Ref	Expression
1		sbthlem.1	. . . . . . . . . . 11
2		sbthlem.2	. . . . . . . . . . 11 $/\$
3	1, 2	sbthlem1 4453	. . . . . . . . . 10
4		imass2 3439	. . . . . . . . . 10
5	3, 4	ax-mp 7	. . . . . . . . 9
6		sscon 2174	. . . . . . . . 9
7	5, 6	ax-mp 7	. . . . . . . 8
8		imass2 3439	. . . . . . . 8
9	7, 8	ax-mp 7	. . . . . . 7
10		sscon 2174	. . . . . . 7
11	9, 10	ax-mp 7	. . . . . 6
12		imassrn 3421	. . . . . . . 8
13		sstr2 2074	. . . . . . . 8
14	12, 13	ax-mp 7	. . . . . . 7
15		difss 2170	. . . . . . . 8
16		ssconb 2173	. . . . . . . 8 $/\$
17	15, 16	mpan2 698	. . . . . . 7
18	14, 17	syl 10	. . . . . 6
19	11, 18	mpbiri 194	. . . . 5
20	19, 15	jctil 292	. . . 4 $/\$
21	1, 15	ssexi 2725	. . . . 5
22		sseq1 2085	. . . . . 6
23		difeq2 2157	. . . . . . . 8
24	23	sseq2d 2092	. . . . . . 7
25		imaeq2 3408	. . . . . . . . 9
26	25	difeq2d 2162	. . . . . . . 8
27		imaeq2 3408	. . . . . . . 8
28		sseq1 2085	. . . . . . . 8
29	26, 27, 28	3syl 20	. . . . . . 7
30	24, 29	bitrd 530	. . . . . 6
31	22, 30	anbi12d 630	. . . . 5